COMMENT ⊗   VALID 00020 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.if false then begin "questions"
C00005 00003	.s(PROVIN,PROVING FACTS ABOUT LISP PROGRAMS)
C00012 00004	.ss(appendpf,Simple properties of append)
C00030 00005	.ss(formal,About Formalizing.)
C00040 00006	.ss(lisplang,Theory of LISP: the Language.)
C00052 00007	.ss(lispsem,Theory of LISP: the Semantics.)
C00062 00008	.ss(lispax,Theory of LISP: Algebraic Axioms.)
C00067 00009	.ss(lispinduct,Theory of LISP: Induction Schemas.)
C00077 00010	.ss(dednrule,Deduction Rules for First-Order Logic.)
C00091 00011	.ss(sortrule,Rules for using restricted variables.)
C00094 00012	.ss(condrule,Conditional Expressions.)
C00099 00013	.ss(lambdarule,Lambda-expressions.)
C00103 00014	.ss(funrule,Introducing facts about recursively defined functions.)
C00128 00015	.ss(predrule,Recursively Defined Predicates.)
C00143 00016	.ss(samefr,The SAMEFRINGE problem.)
C00165 00017	.ss(partitionpf,Correctness of a Program to Partition Lists.)
C00184 00018	.ss(partfunrule,Partial functions and the Minimization Schema.)
C00194 00019	.next page
C00197 00020	.ss(provinex2,Exercises Part2.)
C00204 ENDMK
C⊗;
.if false then begin "questions"

how to deal with sorts and λ-expressions.  
this needs to be adressed in the semantics section and the λrule section


Do we want to add axioms for + q* - etc., or just use well know properties 
of numbers without further ado.

Don't use both "well-founded" and "descending chain condition" except in
just one place.



MG discusses possible formalization of funargs and funvals in thesis.
Main discussion deals with "pure LISP 1.5" (without such frills as
progs).   Also points to use of continuations for semantics of
progs, does not give any details.

The following was lifted from intro to IMPURE: (it is basically wrong)
All these features can be formalized in terms of their effect
on the "state of the computation", and this has been done by
Michael Gordon [1975], but his formalizations seem too complicated
for elementary exposition.  The general idea is to introduce a state
variable qx and to describe the "execution" of expressions as
functions on states that produce new states.

.end "questions"
.s(PROVIN,PROVING FACTS ABOUT LISP PROGRAMS)
.if NOTASSEMBLING then start
.IMPURE: NEXT SECTION!;
.MACHIN: NEXT SECTION!;
.SEARCH: NEXT SECTION!;
.EXTEND: NEXT SECTION!;
.ABSNTX: NEXT SECTION!;
.COMPIL: NEXT SECTION!;
.COMPUT: NEXT SECTION!;
.end

	The theory of computation may be divided into
two parts.  The first is the general
theory of computability including topics like universal functions,
the existence of uncomputable functions, lambda calculus, call-by-name and
call-by-value, and the relation of conditional expression recursion
to other formalisms for describing computable functions.  The
second part, which we will discuss in this chapter emphasizes
techniques for proving particular facts about particular computable
functions.  We will emphasize the use of the techniques
more than their mathematical background.  In fact, we omit proofs of the
the mathematical theorems on which our techniques are based.

	In particular we will explain a method for proving ⊗extensional 
properties of a restricted but powerful class of LISP programs which we call
⊗clean, ⊗pure LISP programs.  An ⊗extensional ⊗property is one that
depends only on the function computed by the program.
That two sort programs compute the same function
and that ⊗append is associative are extensional facts, but
that one sort program does ⊗⊗n%52%*⊗ comparisons and another ⊗⊗n_log_n⊗
comparisons or that one program for ⊗reverse does fewer ⊗⊗cons⊗es than
another are not.  These latter facts are examples of ⊗intensional properties.
⊗Clean LISP programs have no side effects (our
methods require the freedom to replace a subexpression by an equal
expression), and equality refers to the S-expressions and not to
the list structures.  ⊗Pure LISP involves only recursive function
definitions and doesn't use assignment statements.
So far we have only discussed how to write clean and pure LISP
programs.   The constructs to be explained in Chapter {SECTION IMPURE}
will take us out of this realm.
We will see in later chapters how the proof techniques can be extended to
cover a larger class of properties and a larger class of programs.

.new ← false
.if new then begin
	We represent both programs and the properties we want to prove
about them as sentences in first order logic.  The proofs are informal
versions of first order logic proofs.  Therefore, we begin with an
informal exposition of first order logic followed by a first order logic
theory of S-expressions and lists.  Next come techniques for proving
properties of programs known in advance to always terminate.  After this
come the more difficult techniques required when termination cannot be
assumed and termination or non-termination must be proved.
.end

	We shall begin with an informal example and a discussion of the ideas
and principles involved.  We then proceed to formalize these ideas.  
We will give a fairly formal description of the method which is based on the
use of first-order logic.  There will also be many examples of application
of the proof technique.  The working out of example proofs will be 
generally in the usual informal mathematical style and should be understandable
intuitively as well as being formally correct when all the detail is filled in.

	The methods of first-order logic are well
developed and understood.  The reason for wanting a formal system
is that such a system can easily be described to and manipulated by a computer.
Given a program that can understand the description of a first-order
language and can understand proofs about facts stated in this
language, we can describe our technique for proving facts about
LISP programs to this program and it will be able to check that our
proofs are correct.  Such a program exists at Stanford [Weyhrauch 1977].
Other programs exist which are designed to prove facts about LISP programs,
for example [Boyer and Moore 1978].  Much of the material in
this chapter is based on [Cartwright and McCarthy 1979].
An extensive treatment of older program proving techniques
is given in [Manna 1974].

.ss(appendpf,Simple properties of ⊗⊗append⊗)

	Before describing general methods for proving 
properties of LISP programs, we consider
the familiar program for ⊗⊗append⊗ing two lists given by

!fcnappend&3 ⊗⊗⊗u*v ← qif qn u qthen v qelse qa u . [qd u * v]⊗.

We prove that for any lists ⊗u and ⊗v, the program
terminates and that the function ⊗u*v, computed by this program,
has the following properties:
.begin nofill

!eqnlfidapp ⊗⊗⊗ qnil*u = u,     ⊗
!eqnrtidapp ⊗⊗⊗ u*qnil = u,     ⊗
!eqnassocapp ⊗⊗⊗u*[v*w] = [u*v]*w⊗.
.end

The first two statements express the fact is that qnil is the "zero" of
the append operation.  The standard mathematical terminology is to say
that qnil is both a left identity and a right identity for ⊗append.  The
last equation expresses the fact that ⊗append is associative - like
addition and multiplication of numbers.  [Unlike addition and
multiplication of numbers, ⊗append is not commutative, since $$(A_B)$*$$(C_D)$ =
$$(A_B_C_D)$ ≠ $$(C_D)$*$$(A_B)$].  Associativity allows us to omit brackets and
write ⊗u*v*w, because it doesn't matter how the expression is
parenthesized.

	As we saw in Chapter {SECTION WRITIN} the definition of ⊗append 
has the form of recursion that defines a total function on lists.
Thus given lists ⊗u and ⊗v if we use this definition of ⊗append and
the rules for evaluation given in Chapter {SECTION READIN} we will arrive
at an answer in a finite number of steps.  In order to describe the function
thus determined we write the equation

!eqnassocdef ⊗⊗⊗u*v = qif qn u qthen v qelse qa u . [qd u * v]⊗.

All we have done is to replace the "←" sign by "=".   We will assume that
the equation holds for all lists (lists not S-expressions in general) ⊗u 
and ⊗v.  

	Proving ⊗⊗qnil*u = u⊗, i.e. that qnil is a left identity
for ⊗append, is easy.  We just substitute in {eqn assocdef} and get
.begin nofill select 2 turnon "∂"
.n←26; m←20

∂(m)qnil*u ∂(n)= qif qn qnil qthen u qelse qa qnil . [qd qnil * u]
∂(n)= u.
.end


That was untypically easy, because we won't often succeed in proving what
we want just by substituting in function definitions and using known
properties of the elementary LISP functions and conditional expressions.  
In fact, when we want
to prove something about a function defined by recursion, we almost
always have to use some technique of mathematical induction in making
the proof.  Proving that qnil is a right identity {eqn rtidapp} requires such 
an induction.  As before, we begin by substituting into {eqn assocdef}, but
this time we get

⊗⊗⊗u*qnil = qif qn u qthen qnil qelse qa u . [qd u * qnil]⊗,

and this time the conditional expression does not just collapse.
However, notice that if ⊗u were qnil, {eqn rtidapp} would follow.  Notice
also that if ⊗u were not qnil, but we knew that qnil were a right identity for 
⊗⊗qd u⊗, we could make the calculation
.begin nofill select 2 turnon "∂"
.n←30; m←24

∂(m)u*qnil ∂(n)= qa u . [qd u * qnil]
∂(n)= qa u . qd u
∂(n)= u,
.end

and this is what we want to prove.

	The induction technique for proving some proposition for all
⊗u is to prove it under the assumption that it holds for all
"smaller" ⊗u.  We then conclude that it holds for all ⊗u.  
In this case, we are calling a list ⊗w1 "smaller"
than a list ⊗w2 if it is a "tail" of ⊗w2.  In particular ⊗⊗qd u⊗ is
a "tail" of ⊗u and hence "smaller" than ⊗u.  

	The correctness of such an induction technique depends on the
notion of "smaller" satisfying what mathematicians call a "descending
chain condition".  Namely, given an element ⊗u, there must not be
an infinite descending chain of elements starting with ⊗u such that each
element is smaller than the preceding one.  In the case of lists, this is 
informally obvious; if you keep taking sublists, you will eventually arrive at
the null list.

	A descending chain condition is all we need to make induction
work, because if a proposition concerning ⊗u follows from the same
proposition for all smaller elements, then the converse of the same
argument would derive from any counter example a smaller counter
example and hence an infinite descending chain of counter examples.
If there can't be any infinite descending chains at all, then there
can't be an infinite descending chain of counter examples.

	In the above argument, we have avoided mathematical symbolism.
In order to make the method easy to apply, we shall express all this
formally in the following sections.

	Now let us return to our proof of the three properties of ⊗append.  
The associativity of ⊗append {eqn assocapp}
is proved by exactly the same kind of inductive argument as we use for
proving qNIL is a right identity.  In the case of associativity,
the algebra is a little more complicated.  The induction hypothesis is that
⊗append is associative for all "smaller" ⊗u.  There are two cases.

	If ⊗u is qnil, the theorem is an obvious consequence of the
fact that qnil is a left identity, i.e. the first theorem we proved.
(The hypothesis that the theorem is true for all smaller ⊗u played
no role, because there is no list smaller than qNIL).
If ⊗u is not qnil, we have
.begin nofill turnon "∂"
.n←24; m←12 ; l←32;

∂(4)⊗⊗[u*v]*w⊗∂(m)⊗⊗= [qa u . [qd u * v]] * w⊗, ∂(l)using the definition of ⊗⊗u*v⊗,

	      ∂(m)⊗⊗= qa [qa u . [qd u * v]] . [[qd [qa u . [qd u * v]] * w]⊗, 
			∂(n)using the definition of ⊗append to expand the second * of the 
	                ∂(n)previous line together with the fact that ⊗⊗[qa u . [qd u * v]]⊗
			∂(n)cannot be qNIL, since it is formed by a ⊗cons. 

	      ∂(m)⊗⊗= qa u . [[qd u * v] * w]⊗,  ∂(l)simplifying the above using facts about 
			∂(n)qqa and qqd applied to ⊗⊗[qa u . [qd u * v]],⊗

	      ∂(m)⊗⊗= qa u . [qd u * [v * w]]⊗, ∂(l)using the induction hypothesis and the fact
			∂(n)that ⊗⊗qd u⊗ is smaller than ⊗u. 

	      ∂(m)⊗⊗= u * [v * w]⊗, ∂(n+4)using the definition of ⊗append applied to 
			∂(n)the first * in ⊗⊗u*[v*w]⊗, i.e. going backwards.
.end
	The algebra of this proof is rather typical.  We used the definition
of the function involved several times, we used the induction hypothesis
once, and we used the elementary algebraic facts about conditional
expressions and the basic functions of LISP.
Note that in the qNIL case we did not need the induction hypothesis.  With
induction proofs it is generally the case that there are some "base" cases
which are proved directly.  The remaining cases have the property that
they can be reduced to simpler cases, for which the induction hypothesis 
applies.

	If one is willing to do without equations, proving the termination
of ⊗u*v is also easy.  We first note that when ⊗u is qnil, the computation
terminates.  Next we note that if the computation terminates for qd u and
all ⊗v, then the computation of ⊗u*v terminates.  Just as before, we can
make the argument that if there were a counter example to the termination
of ⊗u*v, then there would be an infinite decreasing chain of counter-examples,
and this is impossible.  Notice that this argument is even more informal
than the preceding, because we haven't given a way of expressing termination
as an equation.

	The method we used above works well for programs that define total
functions on lists, S-expressions, numbers, etc.  If we restricted ourselves
to such programs we would be set.  However, it is well known that LISP programs
do not always terminate.  (You have probably written a few such programs yourself!)  
Even if the program does terminate, a large part of our effort in proving
properties is often devoted to proving the termination part as there are
many interesting programs that do not match one of the schemas that are
guaranteed to define total functions.  
Also many interesting programs terminate on some but not all values of the
arguments (for example ⊗⊗eval⊗) and we would like to be able to say things
about these programs.  

	The argument we made above to show directly that ⊗append terminated
was correct, but informal.  We want to introduce a formal notation so that
we can prove termination by explicit rules and thus meet our goal of having
a computer be able to check our proofs.   It turns out that we will be able
to describe a general form of recursive definition which will have the
nice property that we can replace "←" by "=" and compute with the resulting
equation regardless of whether or not the program always halts.   However
we have to careful about using the resulting expressions in contexts
where S-expressions (or lists or numbers) are expected.   To see why this
is so consider the following definition

!fcnomega& ⊗⊗⊗omega x ← omega x . $$A$⊗.

It is easy to see that this program never terminates.  (In a computer you
would probably get an overflow of some kind as the evaluator attempted
to construct an infinite tree of $$A$s. )   Suppose we now form the
corresponding equation

!eqnomegadef ⊗⊗⊗omega x = omega x . $$A$⊗.

and further assume that everything is an S-expression.   Then in particular
⊗⊗omega x⊗ is an S-expression for any ⊗x.   The equation {eqn omegadef} 
says that is not an atom and thus we can apply ⊗car to both sides of the 
equation obtaining

⊗⊗⊗qa omega x = omega x⊗.

This is not possible for a finite tree like structure.   In fact,
applying our induction principle to S-expressions where ⊗⊗qa x⊗ is
"smaller" than ⊗x for non-atomic ⊗x we, can arrive at a contradiction
from this equation.  Having thus proved qfalse we can prove anything
we like (and no-one would believe anything we proved)!   The way out
of this dilemma is to admit non-S-expressions into the domain of things
we are describing by the equations we write.  We will in fact consider
the domain of "extended" S-expressions formed by adding an element, qb,
called "bottom" to the domain of S-expressions.  When a function doesn't
terminate we will assign it this value.  Then we must extend all of our
functions to this larger domain.  For example we will need to say
what happens when qqa and qqd are applied to qb.  If we do this just right
we will have a consistent system, and our proofs will be meaningful.
.skip

.cb Exercises.
.item←0

Prove the following properties of ⊗reverse   

#. 	⊗⊗∀u: reverse u = reverse1 u⊗

#.	⊗⊗∀u v: reverse[u * v] = [reverse v] * [reverse u]⊗

#.  	⊗⊗∀u: reverse reverse u = u⊗.

Recall that ⊗reverse and ⊗reverse1 are defined by

	⊗⊗reverse1 u ← if qn u qthen qNIL qelse [reverse1 qd u] * <qa u>⊗

	⊗⊗reverse u ← rev[u, qNIL]⊗

	⊗⊗rev[u, v] ← qif qn u qthen v qelse rev[qd u, qa u . v]⊗


As with the definition of ⊗append, these definitions are of a form guaranteed
to define a total funtion on lists.   Assume that the defined functions
in each case satisfy the functional equation obtained by 
replacing "←" by  "=".  
(The first proof requires inventing a suitable sentence on which to do an
induction.)

.ss(formal,About Formalizing.)

	Before describing the formal details of the ideas used in the
previous section it is perhaps appropriate to give a preview of what we are
about to do and some explanation as to why.  The main point is to be able to make
the arguments clear and precise.  This wins in several ways.  For
the logicians the development of formal systems and methods of
reasoning allowed them to deal with paradoxes which arose in
informal arguments and also to prove many interesting things about 
their systems.
For the computer scientist formalization
provides a way of making your notions and reasoning precise enough
to be understood and manipulated by a computer.  One goal, of course,
it to have the computer do as much of the work for you as possible.

	Our particular goal is a system in which we can prove
facts about LISP programs and have our proofs checked on a computer.
What do we need in such a system?
First we need a language in which to express facts about S-expressions
and about functions and predicates on S-expressions.   We will assign
"meaning" to some of the expressions of our language by interpreting
them as elements of the domain of extended S-expressions
(S-expressions ∪ α{qb}) or as functions or predicates on this domain.  
Some of the expressions 
(sentences) will be interpreted as having truth values.

	Having specified our language and given meaning to some of the
expressions of this language we have in some sense specified which
sentences are true.  Given a particular sentence we can try to decide
whether or not it is true of our extended S-expression domain.  However
the argument would still be informal and it would not be easy to check that
it is valid.   Thus the next step is to develop a formal method of proof.
The idea is to find a set of rules for deriving true sentences from
a given collection of sentences by successive
application of the rules.  Such a derivation is then a formal proof
that the sentence derived follows from the given sentences.
For a notion of formal proof to be useful we will need
to find a collection of sentences or "axioms" which will 
characterize the domain we are studying in the sense that the true 
sentences can be derived from the axioms using the given proof rules.
(The sad fact is that completely characterizing a domain as rich as
S-expressions by a finite collection of axioms is impossible;
however we can come close enough to provide a useful system.)

	The above may seem like a formidable task, however we are in luck.
Most of the work has been done already as our requirements are met nicely
by what is known as first-order logic.  Logicians have developed a notion
of first-order logic with the form of the language determined, 
a method of assigning meaning to expressions of the language (model theory),
and a "complete" set of proof rules for proving sentences of the language true.
Our task is reduced to filling in the details of
the language specification and deciding on a collection of axioms.
We will do this in the following sections.   We shall also discuss
proof rules in more detail.

	At this point we will have developed a system in which we state and 
prove facts about the extended domain of S-expressions and the primitive 
functions and predicates.  We really wish to be able
to state and prove facts about programs we have written.  For the time being
we will be satisfied with proving things about the function computed by
a given program.  Thus we need to be able to associate a particular 
function with each program and to characterize this function by sentences
in the language, which we then add as additional axioms.
First we must restrict the general form (schema) for recursive definition
so that we can always choose on the corresponding function in a
uniform manner.   We choose as the corresponding function, the function
whose value is that determined by the program if it terminates and 
whose value is qb otherwise.
Having made a suitable choice  of allowed programs, we can
then introduce as an axiom the (fully quantified) equation obtained
replacing "←" in the recursive definition by "=" .
If the program always terminates with an
S-expression value then this equation is sufficient to characterize the
function completely.  Otherwise we need to add additional axioms
expressing the fact that the function is not only a solution to the
equation, but that its value is an S-expression only when the
the computation procedure actually returns an S-expression.  
This collection of axioms is generated from a schema called the
⊗⊗minimization schema⊗.  The name refers to the fact the function
being described is the least defined or minimal solution to the
functional equation.

	Again it seems that we have a fair amount of work to do.  But,
we will be able to use or parallel several results of recursive function
theory to reach our goal.  

	We conclude this section with a summary of steps to be
carried out in order to describe fully our "theory of LISP".
They are
.begin nofill indent 8,8 
.item←0

#.  Define a language and semantics
#.  Give axioms characterizing extended S-expressions
#.  Give rules for proving
#.  Specify the allowed programs
#.  Characterize the function corresponding to an allowed program .
.end

In the remainder of this chapter we will carry out these steps.  
We will also give several example proofs using the techniques we are 
describing.  
The reader unfamiliar with formal systems may find the formal description
and development of the proof system a bit heavy.  One way to approach
it is to skim through the formalities, keeping in mind the plan and
motivation outlined above.  Then put serious effort into understanding
the examples.  After obtaining some facility in using the methods 
the formalities should be more meaningful and easier to understand.
.ss(lisplang,Theory of LISP: the Language.)

	The usual first-order logic has a language consisting of 
terms and formulas built from four collections of (non-logical) symbols: 
constants, variables, functions symbols and predicate symbols,
using application (of a function or predicate to a list of terms),
propositional connectives and quantifiers.   
A term is an expression whose value (meaning) will be an object like an 
S-expression while a formula is either true or false for any particular
assignment of values to the variables occuring free.  
A first-order logic with 
equality has among its predicate symbols a binary symbol (often "=") 
whose interpretation is that of equality between objects of the domain.  

	The logic we shall use is a first order logic with equality,
extended by admitting conditional expressions and first
order lambda-expressions.  Our language will have function and predicate
expressions in addition to terms and formulas.  These expressions will
be treated like complicated function and predicate symbols.  
These extensions 
do not change the logical strength of the theory, because, as we shall see, every
formula that includes conditional expressions or first order lambdas can be
transformed into an equivalent formula without them.  However, the
extensions are practically important, because they permit us to use
recursive definitions directly as formulas of the logic.  
Also we will have various "sorts" of variables, each sort restricted
to range over some subset of the domain of interest
rather than over all objects.  We can then restrict
the domain of a function to some fixed subdomian.  
This is mainly a formal shorthand,
it allows us to write formulas that are much shorter and easier to read.
Again any formula written in this shorthand notation can be expanded 
in terms of unrestricted variables.  When using the shorthand notation one
needs to be somewhat more careful in applying the proof rules, but
it seems to be worth the effort in the long run.  We have in fact been using
the sorting conventions informally in the preceeding chapters, so you
are probably already used to them.
For example, we use the variables ⊗u and ⊗v to denote lists, and our
recursive definitions for functions on lists are given in terms of these
list variables to indicate that we are not specifying what the result
will be for non-list input.

	The four classes of symbols of our language are as follows.

%3Constants%1: We will use S-expresssions as constants standing for
themselves.  In particular we will have the atom qNIL. 
We will use the usual symbols $0, $1, ..., for atoms that represent numbers.  
Among the non-S-expression  constants we will have qb (read "bottom").

%3Variables%1: We will use the letters ⊗X, ⊗Y, ⊗Z 
as general variables ranging over the extended S-expressions  
(the set consisting of S-expressions togther with the constant qb).
The variables ⊗u, ⊗v, ⊗w  will range over lists, 
while ⊗x, ⊗y, ⊗z will range over S-expressions.
⊗k, ⊗l, ⊗m, ⊗n are integer variables.  
The variables may appear with or without subscripts.

%3Function symbols%1:  The collection of function symbols contains
the LISP function names qqa, qqd and "." (as an infix).
Other function symbols including function parameter symbols 
will be introduced as needed.

%3Predicate symbols%1: 
As predicate constant symbols we will use the logical equality symbol =, and
the LISP predicate names qqat, qqn and qeq.  
We will use qP as a predicate parameter symbol.  We will also use the
unary predicate symbols  ⊗sexp, ⊗list and ⊗natnum.  
Other predicate symbols will be introduced when needed.

	We suppose that each function and predicate symbol takes the same 
definite number of arguments every time it is used.  
(This number is called the "arity".)  
We will use informally the notation such as ⊗⊗<xq1, ... ,xq->⊗ 
to represent the list forming functions,  but 
formally this should be considered as an abbreviation for
⊗⊗xq1 . [ ... [xq- . qNIL] ... ]]⊗.   
We will often use one argument function and predicate symbols as prefixes, i.e.
without brackets, just as qqa, qqd, etc. have been used up to now.
Two argument function and predicate symbols will also be used as infixes
where customary.

	Next we define terms, formulas, function expressions
and predicate expressions inductively.  
Terms are used in making formulas, and formulas occur in
terms so that the definitions are ⊗mutually ⊗recursive where
this use of the word ⊗recursive should be distinguished from
its use in recursive definitions of functions.
Function and predicate expressions are also involved in the mutual recursion.


%3Terms%1: Constants are terms, and variables are terms.  If
qq is a function expression taking ⊗n arguments, and ⊗⊗tq1,_..._,tq-⊗
are terms, then ⊗⊗qq[tq1,_..._,tq-]⊗ is a term.  If ⊗s is
a formula and ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are terms, then
[⊗⊗qif_s_qthen_tq1_qelse_tq2⊗] is a term.  
Some examples of terms in our language are:
.begin nofill turnon "∂" group
.n←24

∂(n)   (i)   qNIL
∂(n)  (ii)   ⊗⊗x⊗
∂(n) (iii)   ⊗⊗qa x⊗
∂(n)  (iv)   ⊗⊗[λx: qif qat x qthen z qelse qd x][assoc[z,u]]⊗

.end

%3Function expressions%1: A function symbol is a function expression.
If ⊗⊗qxq1,_..._,qxq-⊗ are variables and ⊗t is a term, then
⊗⊗[λqxq1,_..._,qxq-:_t]⊗ is a function expression.

%3Predicate expressions%1: A predicate symbol is a predicate expression.
If ⊗⊗qxq1,_..._,qxq-⊗ are variables and ⊗s is a formula, then
⊗⊗[λqxq1,_..._,qxq-:_s]⊗ is a predicate expression.

Some examples of function and predicate expressions are:
.begin nofill turnon "∂" group
.n←24

∂(n)   (v)   qa 
∂(n)  (vi)   ⊗⊗issexp⊗
∂(n) (vii)   ⊗⊗λx: qif qat x qthen z qelse qd x⊗

.end

.xgenlines←xgenlines-2

%3Formulas%1:
If ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are terms then ⊗⊗tq1_=_tq2⊗ is a formula.
If qp is a predicate expression taking ⊗n arguments and
⊗⊗tq1,_..._,tq-⊗ are terms, then ⊗⊗qp[tq1,_..._,tq-]⊗ is
a formula.
If ⊗s is a formula, then ¬⊗s is also a formula.  If
⊗⊗sq1⊗ and ⊗⊗sq2⊗ are formulas, then ⊗⊗sq1⊗_∧_⊗⊗sq2⊗, 
⊗⊗sq1⊗_∨_⊗⊗sq2⊗, ⊗⊗sq1⊗_⊃_⊗⊗sq2⊗, and
⊗⊗sq1⊗_≡_⊗⊗sq2⊗ are formulas.  If ⊗⊗sq0⊗, ⊗⊗sq1⊗ and ⊗⊗sq2⊗ are
formulas, then [⊗⊗qif_sq0_qthen_sq1_qelse_sq2⊗] is a formula.
If ⊗⊗qxq1,_...,_qxq-⊗ are variables, and ⊗s is a formula, then
⊗⊗[∃qxq1_..._qxq-:_s]⊗ and ⊗⊗[∀qxq1_..._qxq-:_s]⊗ are formulas.
Some examples of formulas are:
.begin nofill turnon "∂" group
.n←24

∂(n)(viii)   ⊗⊗qa x = qd x⊗
∂(n)  (ix)   ⊗⊗issexp X⊗
∂(n)   (x)   ⊗⊗qif qn u ∨ qn qd u qthen qtrue qelse qa u = qad u⊗
∂(n)  (xi)   ⊗⊗∀x: [¬qat x ⊃ ∃y z: x = y . z]⊗

.end

	An occurrence of a variable qx is called ⊗bound if
it is in an expression of one of the forms ⊗⊗[λqxq1_..._qxq-:_t]⊗,
⊗⊗[λqxq1_..._qxq-:_s]⊗, ⊗⊗[∀qxq1_..._qxq-:_s]⊗ or ⊗⊗[∃qxq1_..._qxq-:_s]⊗
where qx is one
of the numbered qx's.  An occurrence that is not bound is called ⊗free.  
A formula having no free variables is called a ⊗sentence.  
Thus ⊗x is bound in example (iv) (of terms) but ⊗z and ⊗u are not.
⊗u is free in example (x) and example (xi) is a sentence.
.ss(lispsem,Theory of LISP: the Semantics.)

	The ⊗semantics of first order logic consists of the rules
that determine whether a formula is true
or false.  However, the truth or falsity of a formula is relative
to the interpretation assigned to the constants, free variables, function and predicate
symbols of the formula as objects of, or functions and predicats on, some domain.

	The domain we are interested in is the extended S-expressions, eg.
S-expressions together with the element qb.   We assign meaning to an expression
of our language inductively in a manner similar to the method of defining
the language itself.  Terms will denote S-expressions or qb, function expressions
will be assigned functions on extended S-expressions, predicate expressions will
be assigned predicates on extended S-expressions, and formulas will be determined
to be true or false.   

	The meaning assigned to constants, and to function and predicate
symbols will be fixed.  
The symbol qb and any S-expression constants appearing in an expression
will stand for themselves.  
Each function or predicate constant symbol is assigned a
function or predicate on the domain.  We will normally assign to the
basic LISP function and predicate symbols the corresponding basic LISP
functions and predicates.  Thus qqa, qqd, ".", qqat, qqn, and qeq will
have their usual meaning.  The equality symbol, "=", will also have its
usual meaning.   The predicate ⊗sexp will be true only for arguments 
that denote S-expressions, similarly ⊗list will be true only for lists
and ⊗numberp will be true only for atoms representing numbers.
Function and predicate parameter symbols do not get assigned any meaning.
Their use is mainly in writing axiom schemata from which an axiom can
be obtained by substituting an actual function or predicate expression 
for the parameter.  

	A particular interpretation is determined by the
values assigned to variables.   In principle to completely determine an
interpretation each variable must be assigned an element of the domain.
In practice we will only worry about variables appearing free in the
expression to which we are interested in assigning a value.
A general variable maybe assigned any element of the domain.  
A variable restricted to range over S-expressions may only be assigned
S-expression values.  Similarly variables restricted to range over
lists or numbers may only be assigned values that are list or atoms
denoting numbers, respectively.

	If qq is a function expression taking ⊗n arguments, 
and ⊗⊗tq1,_..._,tq-⊗ are terms, then the value assigned to
⊗⊗qq[tq1,_..._,tq-]⊗ is the value of the function assigned to qq
when applied to arguments having the values assigned to the terms ⊗⊗t%4i%*⊗.
If ⊗s is a formula and ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are terms, then
if ⊗s is true the value of the term [⊗⊗qif_s_qthen_tq1_qelse_tq2⊗] is
the value of  ⊗⊗tq1⊗ otherwise (⊗s must be false and) the value of
the term is the value of ⊗⊗tq2⊗.

	⊗⊗[λqxq1_..._qxq-:_e]⊗ is assigned a function or predicate according
to whether ⊗e is a term or a formula.  The value of 
⊗⊗[λqxq1_..._qxq-:_e][tq1,...,tq-]⊗ is obtained by evaluating the 
⊗⊗t⊗'s and using these values as values of the qx's in the
evaluation of ⊗e.  If ⊗e has free variables in addition to the qx's,
the function or predicate assigned will depend on them too.

	If ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are terms then ⊗⊗tq1_=_tq2⊗ is true
exactly if ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are are assigned the same value in the domain.
If qp is a predicate expression taking ⊗n arguments and
⊗⊗tq1,_..._,tq-⊗ are terms, then ⊗⊗qp[tq1,_..._,tq-]⊗ is
true exactly when the tuple of values assigned to the ⊗⊗t%4i%*⊗'s satisfies the 
predicate assigned to qp.
If ⊗s is a formula, then ¬⊗s is true exactly when ⊗s is false. 
If ⊗⊗sq1⊗ and ⊗⊗sq2⊗ are formulas, then the truthvalues of the
formulas ⊗⊗sq1⊗_∧_⊗⊗sq2⊗, 
⊗⊗sq1⊗_∨_⊗⊗sq2⊗, ⊗⊗sq1⊗_⊃_⊗⊗sq2⊗, and
⊗⊗sq1⊗_≡_⊗⊗sq2⊗ are determined from the truth values of the
formulas ⊗⊗sq1⊗ and ⊗⊗sq2⊗ according to the following table:
.xgenlines←xgenlines-2
.begin nofill turnon "∂" 
.group
.n1←20;n2←28;n3←36;n4←44;n5←52;n6←60;

∂(n1+1)⊗⊗sq1⊗∂(n2+1)⊗⊗sq2⊗∂(n3+1)∧∂(n4+1)∨∂(n5+1)⊃∂(n6+1)≡

∂(n1)qtrue∂(n2)qtrue ∂(n3)qtrue∂(n4)qtrue∂(n5)qtrue∂(n6)qtrue
∂(n1)qtrue∂(n2)qfalse∂(n3)qfalse∂(n4)qtrue∂(n5)qfalse∂(n6)qfalse
∂(n1)qfalse∂(n2)qtrue∂(n3)qfalse∂(n4)qtrue∂(n5)qtrue∂(n6)qfalse
∂(n1)qfalse∂(n2)qfalse∂(n3)qfalse∂(n4)qfalse∂(n5)qtrue∂(n6)qtrue

!tabletruth The semantics of logical connectives.!
.end

If ⊗⊗sq0⊗, ⊗⊗sq1⊗ and ⊗⊗sq2⊗ are formulas, then if ⊗s is true, 
[⊗⊗qif_sq0_qthen_sq1_qelse_sq2⊗] is true exactly when ⊗⊗sq1⊗ is true and 
if ⊗s is false 
[⊗⊗qif_sq0_qthen_sq1_qelse_sq2⊗] is true exactly when ⊗⊗sq2⊗ is true.
If ⊗⊗qxq1,_...,_qxq-⊗ are variables, and ⊗s is a formula, then
⊗⊗[∀qxq1_..._qxq-:_s]⊗ is qtrue if and only if ⊗s is 
qtrue for ⊗all allowed assignments of elements of the domain to the qx's.  
An assignment is allowed if the variable is general or if it is restricted 
and it is assigned a value in the subdomain to which it is restricted.
If ⊗s has free variables that are not among the qx's, then the
truth of the formula depends on the values assigned to these remaining
free variables.  ⊗⊗[∃qxq1_..._qxq-:_s]⊗ is true if and only if ⊗s is
true for ⊗some allowed assignment of elements of the domain to
the qx's.  Free variables are handled just as before.

	Those who are familiar with the lambda calculus should note
that λ is being used here in a very limited way.  Namely, the variables
in a lambda-expression take only elements of the domain as values,
whereas the essence of the lambda calculus is that they take arbitrary
functions as values.  We may call these restricted lambda expressions
⊗⊗first-order lambdas⊗.  
.ss(lispax,Theory of LISP: Algebraic Axioms.)
 
	We now turn to the task of giving the axioms of our theory of LISP.
The axioms are divided into several groups.  First are some "bookkeeping"
axioms describing the relations between subdomains, particular elements 
of these subdomains and the domains and ranges of the basic functions of LISP.
Next there are the "algebraic" axioms giving the relations satisfied by the
basic LISP functions.  Finally come the induction axioms.  They are in
fact axiom schemata and have the effect of providing an infinite collection
of axioms, one for each instance of a schema.   The axioms are given names
either individually or in small groups for later reference.
To refer to the second axiom in a group named $AXNAME we write $AXNAME2.  

.turnon "∂"

.bb Bookkeeping axioms.

	We recall that ⊗x, ⊗y and ⊗z are asserted to range over S-expressions
and thus will satisfy ⊗issexp.  Similiarly ⊗u, ⊗v and ⊗w will satisfy ⊗islist 

$SEXP:          ∂(16)⊗⊗∀X:[islist X ⊃ issexp X]⊗

                ∂(16)⊗⊗∀X: qat X ⊃ issexp X⊗

                ∂(16)⊗⊗¬issexp qb⊗

$NIL:           ∂(16)⊗⊗islist qNIL⊗

$NULL:          ∂(16)⊗⊗∀u: [qn u ≡ u=qNIL]⊗

                ∂(16)⊗⊗∀u: [qn u ≡ qat u]⊗

$CONS:          ∂(16)⊗⊗∀x y: ¬qat [x . y]⊗

                ∂(16)⊗⊗∀x y: issexp [x . y]⊗

                ∂(16)⊗⊗∀x u: islist [x . u]⊗

$CAR:           ∂(16)⊗⊗∀x: [¬qat x ⊃ issexp qa x]⊗

$CDR:           ∂(16)⊗⊗∀x: [¬qat x ⊃ issexp qd x]⊗

                ∂(16)⊗⊗∀u: [¬qn u ⊃ islist qd u]⊗


.bb  Algebraic axioms. 

$CAR-CONS:      ∂(16)⊗⊗∀x y: qa [x . y] = x⊗

$CDR-CONS:      ∂(16)⊗⊗∀x y: qd [x . y] = y⊗

$EQ-CONS:       ∂(16)⊗⊗∀x: [¬qat x ⊃ [qa x . qd x] = x]⊗   


	An alternate form of $EQ-CONS which we will find useful is

$EQ-SEXP:       ∂(16)⊗⊗∀x y: [[¬qat x ∧ ¬qat y] ⊃ [qa x = qa y ∧ qd x = qd y ≡ x = y]] ⊗.
 

	These axioms are analogous to the algebraic part of Peano's
axioms for the non-negative integers.  The analogy can be made clear
if we write Peano's axioms using ⊗n' for the successor of ⊗n and
⊗⊗n⊗%5-%* for the predecessor of ⊗n.  Peano's algebraic axioms
then become

$ZERO:		∂(16)⊗⊗numberp $$0$⊗

$ADD1:         	∂(16)⊗⊗∀n: n' ≠ $0 ⊗

$SUB1:          ∂(16)⊗⊗∀n: (n')%5-%* = n ⊗

$SUB_ADD:       ∂(16)⊗⊗∀n: n ≠ $0 ⊃ (n%5-%*)' = n ⊗.


Lists could be used to model integers in many ways.  For example, we could
represent the number ⊗n by a list of ⊗n qNILs.
We would then have
⊗⊗n'_=_cons[qNIL,n]⊗ and ⊗⊗n%5-%*_=_qd n⊗.  

.turnoff
.ss(lispinduct,Theory of LISP: Induction Schemas.)

	Clearly S-expressions and lists satisfy the axioms given for them,
but unfortunately these algebraic axioms are insufficient to characterize them.  
For example, consider a domain of one element  ⊗a satisfying

⊗⊗⊗qa a = qd a = a . a = a .		⊗

It satisfies the algebraic axioms for S-expressions.  We can exclude
it by an axiom ⊗⊗∀x: [qa x ≠ x]⊗, but this won't exclude other
circular list structures that eventually return to the same element
by some qqa-qqd chain.  Actually we must exclude all infinite
chains, because list structures are finite object, and every
qqa-qqd chain eventually terminates in an atom.  This cannot be
done by any convenient finite set of axioms.   
As we mentioned earlier most proofs of properties of LISP programs will
require applying some induction principle.   
Requiring that our domain satisfy certain induction principles allows us 
to exclude circular and infinite list structures.

	The general form of a proof
by induction uses a relation which tells us when one element is "smaller" than
another.  If we can prove that a property, qP, holds for some element by assuming
that it holds for all smaller elements then we can conclude that qP holds
for all elements of the domain.   This a valid proof as long as the relation
is "well-founded", e.g., as long as it satisfies the descending chain condition
described in section qsect{subsection appendpf}.

	We will express our induction principles in the form of axiom schemas
using qP as a predicate parameter.   We obtain
instances of the schema by substituting particular predicates for qP.
It is called an axiom schema rather than an axiom, because we consider
the schema, which is not properly a sentence of first order logic, as
standing for the infinite collection of axioms that arise from it by
substituting all possible predicate expressions of our language for qP.

	For example over the domain of natural
numbers the usual "<" relation is well-founded and gives rise to
the form of induction usually called "course of values" induction.
The schema obtained using this relation is
.turnon "∂"

$NUMBINDUCTION-CVI: ∂(28)⊗⊗∀n: [∀m: [m < n ⊃ qP m] ⊃ qP n] ⊃ ∀n: qP n⊗

If we use the predecessor relation and notice that each non-zero number
has just one predecessor we obtain the schema

$NUMINDUCTION: ∂(24)⊗⊗qP $0 ∧ ∀n: [n≠$0 ∧ qP n-$1 ⊃ qP n] ⊃ ∀n: qP n⊗

which corresponds to the usual form of induction given in axiomatizations 
of number theory (for example Peano's axiomatization).

	We also need induction principles for lists and for S-expressions,
and for this we need ordering relations corresponding to ≤ and <.  For lists
these relations are called ⊗istail and ⊗isptail.  We write ⊗⊗u istail v⊗
to mean that the list ⊗u is a tail of the list ⊗v.  Thus $$(C D)$ ⊗istail 
$$(A B C D)$.  ⊗⊗u isptail v⊗ means that ⊗u is a proper tail of ⊗v, i.e.
equality is excluded.  If ⊗u is non null we will have ⊗⊗qd u istail u⊗.

	⊗istail is given by the simple LISP program

⊗⊗⊗u istail v ← u = v ∨ ¬qn v ∧ u istail qd v,⊗

but it has a special role in the theory, because it is used in the axiom
schema of induction.  Taking some of its properties as axiomatic, we can
prove the properties of other functions and predicates.

	⊗isptail is defined in terms of ⊗istail by the LISP program

⊗⊗⊗u isptail v ← u ≠ v ∧ u istail v⊗

.if false then begin
	For lists the predecessor of a list ⊗u is ⊗⊗qd u⊗, and we shall use 
the relation ⊗istail corresponding to the "≤" relation to obtain an analogue to <.
⊗istail satisfies the equivalence

!eqnistaildef ⊗⊗⊗∀u v: [u istail v ≡ [u=v] ∨ [¬qn v ∧ u istail qd v]]⊗.

As we shall see later this is a well-defined relation.  In fact
we will see that it is "computable" by a simple recursive program.
Like ≤ it is reflexive, anti-symmetric and transitive.  
The relation ⊗isptail given by

!eqnisptaildef ⊗⊗⊗∀u v: [u isptail v ≡ [u≠v] ∧ u istail v]⊗.

is the desired well-founded relation.  (The "p" stands for "proper".)
The corresponding axiom schemas for lists are:
.end

	Now we can write the axiom schemata for lists which are

$LISTINDUCTION: ∂(20)⊗⊗∀u: [qn u ⊃ qP u] ∧ ∀u: [¬qn u ∧ qP qd u ⊃ qP u] ⊃ ∀u: qP u ⊗.

$LISTINDUCTION-CVI: ∂(24)⊗⊗∀u: [∀v: [v isptail u ⊃ qP v] ⊃ qP u] ⊃ ∀u: qP u⊗

The correctness of this schema depends on the fact that ⊗isptail is a well
founded relation, i.e. you can't keep on taking proper tails forever.

	The corresponding induction principles for S-expressions depend on
the fact that a non-atomic S-expression ⊗x has two "predecessors", ⊗⊗qa x⊗
and ⊗⊗qd x⊗.
The analogues to ⊗istail and ⊗isptail are ⊗subexp and ⊗psubexp.  
⊗subexp is given by the program

	x subexp y ← x = y ∨ ¬qat y ∧ [x subexp qa y ∨ x subexp qd y]

and ⊗psubexp by

	x psubexp y ← x ≠ y ∧ x subexp y.

.if false then begin
As with ⊗istail we shall see later how to define the ⊗subexp relation starting 
with an LISP program.  We now define ⊗psubexp by

!eqnpsubexpdf ⊗⊗⊗∀u v: [u psubexp v ≡ [u≠v] ∧ u subexp v]⊗.
.end

The S-expression induction schemas are

$SEXPINDUCTION: ∂(20)⊗⊗∀x: [qat x ⊃ qP x] ∧ ∀x: [¬qat x ∧ qP qa x ∧ qP qd x ⊃ qP x] ⊃ ∀x: qP x ⊗.

$SEXPINDUCTION-CVI: ∂(28)⊗⊗∀x: [∀y: [y subexp x ⊃ qP y] ⊃ qP x] ⊃ ∀x: qP x⊗


	These schemas are called principles of ⊗structural ⊗induction, 
since the induction is on the structure of the entities involved. Other schemas
derived from principles of ⊗structural ⊗induction are possible and the best schema 
to use depends stongly on the problem at hand.  Some examples will be given in a 
later section.

	Even the axiom schemas don't assure us that the only domain
satisfying the axioms is that of the integers or the S-expressions as
the case may be.  Any first order theory whose axioms
can be given effectively admits the so-called ⊗non-standard_models.  
However, it seems likely that the non-standard models of S-expressions,
like the non-standard models of integers, will agree with the standard
model for sentences of practical interest.


.ss(dednrule,Deduction Rules for First-Order Logic.)

	In section qsect{subsection lispsem} we described how to assign meaning 
to expressions of our language relative to a particular domain ---
the extended S-expressions.  This process could be carried for other
suitable domains and leads to the study of "model theory".  (A domain
together with the assignments to constants, function and predicate
symbols is called a model of the language.)  This is the "semantic"
approach to investigating notions such as truth and validity.
Any particular statement may be true in all models, in some models, or in no models.
Deciding whether a particular statement is true in a particular model will
mean reasoning about the model, perhaps doing some "calculation" in the model, 
or finding a particular object with some given property or showing that 
some property holds for all objects in the model.

	So far we have no precise statement of what it means to show (prove)
that a statement is true.   This is necessary if there is to be any hope
of having the computer help us with proofs.
If we study the rules for determining the truth value of a statement
relative to a particular model
we can arrive at various rules that say whenever some collection of
formulas ⊗⊗sq1⊗, ... ,⊗⊗sq-⊗ are true then some formula ⊗s is
also true.  For example if ⊗⊗sq1⊗ and ⊗⊗sq1⊃sq2⊗ are true
then we see that ⊗⊗sq2⊗ must also be true.  We can also see that some
formulas are true regardless of the meaning assigned to the symbols occuring
in them.  Thus if ⊗s is a formula, then ⊗⊗s ⊃ s⊗ is always true.
A formal proof system is a collection of formulas (axioms)
together with a collection of deduction rules.
A formal proof of a formula ⊗s is a sequence of formulas 
⊗⊗sq1⊗, ... ,⊗⊗sq-⊗ where ⊗⊗sq-⊗ is ⊗s and each ⊗⊗s%4i%*⊗ is either 
one of the axioms, or follows from the preceeding formulas by one of the 
deduction rules.  The study of such systems is known as "proof theory".
It is the syntactic approach to the investigation of truth and validity.
The truth of the basic axioms follows from their syntactic form and
does not depend on what meaning is assigned to particular symbols.
Similarly the validity of the rules follows from the form of the
formulae to which they apply and not their meaning.

	Below we describe a collection of basic axioms 
and deduction rules for one possible formal proof system for first-order logic with 
equality (without conditional expressions, lambda expressions or variables with
restricted ranges).  In the following three
sections we give additional rules for manipulating formulas containing variables 
with restricted ranges, conditional expressions and lambda expressions
which allow us to extend the system to our logic.
To obtain a proof system for our theory of LISP we need only add the
axioms given in sections qsect{subsection lispax} and qsect{subsection lispinduct}
(plus any additional axioms resulting from the introducion of function definitions).
The system we give is very simple to describe, and nice if we wanted to
prove things about the system itself.   For a system to be useful
as a proof system in which to carry out proofs we would prefer
a larger collection of rules that would allow more natural proofs.
Such systems exist, but are correspondingly more complicated to explain
and we will not discuss them here.

.cb Basic axioms.

	The axioms of our basic theory fall into  three groups: tautologies,
axioms for quantifiers, and axioms for equality.  

.bb Tautologies
	A tautology is a formula that is true by virtue of its propositional form.  
For example ⊗⊗sq1_⊃_sq1⊗, ⊗⊗sq1_⊃_[sq2_⊃_sq1]⊗ 
and ⊗⊗sq1_⊃_[sq1_∨_sq2]⊗ are tautologies for any formulas ⊗⊗sq1⊗ and ⊗⊗sq2⊗.
Let ⊗⊗sq1⊗, ⊗⊗sq2⊗,_..._⊗⊗sq-⊗ be formulas and let ⊗s be a formula built 
from the ⊗⊗s%4i%*⊗ using ¬, ∧, ∨, ⊃, and ≡.  Then
We say that ⊗s is a tautology if under all possible combinations of
assignments of qtrue and qfalse to the formulas ⊗⊗s%4i%*⊗ the 
value of ⊗s is qtrue (according to the truth tables).
Every formula that is a tautology is one of our basic axioms.
All tautologies can be deduced from a few basic tautologies, but since
computers can readily test for tautology, we might as well make them
axioms in our theory.

.bb Axioms for quantifiers
Let ⊗⊗sq1⊗ and ⊗⊗sq2⊗ be formulas and qx be a variable that is not free 
in ⊗⊗sq1⊗ then any formula of the form 

!eqnqax1 ⊗⊗⊗∀qx: [sq1 ⊃ sq2] ⊃ [sq1 ⊃ ∀qx: sq2]⊗ 

is one of the basic axioms.
Let ⊗s be a formula, qx a variable and ⊗t a term such that ⊗t may be substituted 
for all free occurrences of qx in ⊗s without any "catching of free variables".
Let ⊗s' be the result of this substitution then any formula of the form

!eqnqax2 ⊗⊗⊗∀qx: s ⊃ s'                       ⊗ 

is one of the basic axioms.  Finally,
if ⊗s is any formula and qx is any variable then any formula of the form

!eqnqax3 ⊗⊗⊗[∃qx: s] ≡ [¬∀qx: ¬s]             ⊗

is one of the basic axioms.

.xgenlines←xgenlines-2

.bb Axioms for equality
	The formula {eqn eax1} is one of the basic axioms.

!eqneax1 ⊗⊗⊗∀X: X = X                         ⊗

	Let ⊗s be a formula, and qx, qxq1, qxq2 be variables 
such that substituting qxq1 or qxq2 for qx in ⊗s does not result
in binding of either variable, and let ⊗⊗sq1⊗ and ⊗⊗sq2⊗ be the
results of that subsitution.  Then any formula of the form {eqn eax2}
is one of the basic axioms.

!eqneax2 ⊗⊗⊗∀qxq1 qxq2: [qxq1 = qxq2 ⊃ sq1 = sq2]⊗

	Similarly, let ⊗t be a formula, and qx, qxq1, qxq2 be 
variables such that substituting qxq1 or qxq2 for qx in ⊗t does 
not result in binding of either variable, and let ⊗⊗tq1⊗ and ⊗⊗tq2⊗ be the
results of the subsitution.  Then a formula of the form {eqn eax3}
is one of the basic axioms.

!eqneax3 ⊗⊗⊗∀qxq1 qxq2: [qxq1 = qxq2 ⊃ tq1 = tq2]⊗

.cb Deduction rules

	There are two deduction rules for the formal proof system:
⊗modus_ponens and ⊗universal_generalizaton.  

.bb Modus Ponens
	The rule known as modus ponens ($$MP$) states that if 
⊗⊗sq1⊗ and sq2⊗ are formulas and if we have proved ⊗⊗sq1⊗ and 
⊗⊗sq1⊃sq2⊗ then we can deduce ⊗⊗sq2⊗.  This is the rule that
we discussed above.


.bb Universal Generalization
	The universal generalization rule ($$UG$), also known as
"∀" introduction, says that if we have proved the formula ⊗s 
then we may deduce ⊗⊗∀qx.s⊗ for any variable qx.


.cb Example

	As a simple demonstration of the use of this formal system we
will give a formal proof of ⊗⊗issexp qNIL⊗ in the system obtained by
adding the axioms $SEXP1 and $NIL (from the LISP algebraic axioms 
section qsect{subsection lispax}) to the basic system.  The proof is as follows:
.begin nofill turnon "∂"
.n←12;m←60
.item←0

∂(n)#.  ⊗⊗∀X:[islist X ⊃ issexp X]⊗∂(m)$$SEXP1$
∂(n)#.  ⊗⊗∀X:[islist X ⊃ issexp X] ⊃ [islist qNIL ⊃ issexp qNIL]⊗∂(m){eqn qax2}
∂(n)#.  ⊗⊗islist qNIL ⊃ issexp qNIL⊗∂(m)$$MP$ 1,2 
∂(n)#.  ⊗⊗islist qNIL⊗∂(m)$$NIL$
∂(n)#.  ⊗⊗issexp qNIL⊗∂(m)$$MP$ 3,4 
.end

	The main point of introducing formal proofs is to
show you that the rules are fairly simple and can be made sufficiently precise
that a computer program could be written to decide whether or not a give rule
applies to a particular situation and when it does apply to carry out the
corresponding proof step.   

	You may at this point ask what such a formal proof
system has to do with our goal of proving statements about the domain
of extended S-expressions.  The connection is the following.  We have
already fixed a language.  Suppose we fix a collection of statements (axioms)
which are true for S-expressions.   Then any statement
formally provable from these axioms will be
true of S-expressions and any statement which is true in %3all%* domains
which "model" our language and in which our axioms 
are true will be formally provable from the axioms.
The snag is that in the case of structures as complex as S-expressions,
for any "reasonable" collection of axioms there will always be domains other than
the extended S-expression domain which "model" the axioms, and there
will be statements true for S-expressions that will not be true for
for some other model and hence the statement will not be formally provable.
Fortunately it is possible to pick a collection of axioms such
these statements do not arise very often and we will generally be able
to find formal proofs for the statements we are interested in proving.
.ss(sortrule,Rules for using restricted variables.)

	The rules we gave for manipulating quantifiers in the previous
section  apply to variables that range over the entire domain.  In order
to handle variables restricted to range over some subset we must either
modify the rules or show how to eliminate the restricted variables from
a formula.  

	Suppose the variable qx is restricted to range over the subdomain
satisfying ⊗isD and the variable qxq1 is a general variable.  
For example, in the case of extended S-expressions we have the subdomain
characterized by ⊗issexp, the variable ⊗x ranging over this domain and ⊗X   
is a general variable.
The formula ⊗⊗∀qx.s⊗ is then equivalent to ⊗⊗∀qxq1:[isD_qxq1_⊃_s]⊗ and
the formual ⊗⊗∃qx.s⊗ is equivalent to ⊗⊗∃qxq1.[isD qxq1 ∧ s]⊗.
If we use the this elimination process directly it defeats the purpose of
introducing the restricted variables in the first place.  As we now have
back all of the extra implications that we did not want to see in the
first place.
Thus we would like to modify the proof rules to make better use of
the abbreviations.

	The only modification required is the axiom schema {eqn qax2}
which is the rule for instantiating a universially quantified
variable to some term.  Here we require that we have also proved
that the term ⊗t is an element of the domain to which the variable qx
is restricted, eg.,
that ⊗⊗isD t⊗ is true.  Alternately we could write the schema

{eqn qax2!} ') ⊗⊗⊗[∀qx: s] ⊃ [isD t ⊃ s']           ⊗ 

and remove the second implication by an application of modus ponens.

.ss(condrule,Conditional Expressions.)

	All the properties we shall use of conditional terms follow
from the relation

!eqncond1 ⊗⊗⊗[s ⊃ [qif s qthen a qelse b] = a] ∧ [¬s ⊃ [qif s qthen a qelse b] = b] ⊗.

	It is worthwhile to list separately some properties
of conditional terms.  First we have the obvious
.begin nofill group

⊗⊗⊗[qif qtrue qthen a qelse b] = a		⊗
!eqncond2 
⊗⊗⊗[qif qfalse qthen a qelse b] = b .		⊗
.end

Next we have a ⊗distributive ⊗law for functions applied
to conditional terms, namely

!eqncond4 ⊗⊗⊗f[qif s qthen a qelse b] = qif s qthen f[a] qelse f[b] ⊗.

This applies to predicates as well as functions and can also be used
when one of the arguments of a function of several arguments is a
conditional term.  It also applies when one of the terms of
a conditional term is itself a conditional term.

Thus
.begin nofill group

!eqncond5 ⊗⊗⊗qif [qif r qthen sq1 qelse sq2] qthen a qelse b =					⊗
⊗⊗⊗qif r qthen [qif sq1 qthen a qelse b] qelse [qif sq2 qthen a qelse b]⊗
and
⊗⊗⊗qif r qthen [qif s qthen a qelse b] qelse c =						⊗
!eqncond6 ⊗⊗⊗qif s qthen [qif r qthen a qelse c] qelse [qif r qthen b qelse c] .		⊗
.end
	When the expressions following qthen and qelse are
formulas, then the conditional expression can be replaced by a formula
according to

!eqncond7 ⊗⊗⊗[qif r qthen sq1 qelse sq2] ≡ [r ∧ sq1] ∨ [¬r ∧ sq2] ⊗.

These rules permit eliminating conditional expressions from formulas
by first using distributivity to move the conditionals
to the outside of any functions or predicates and then replacing the conditional
expression by a Boolean expression.   They could be added to our formal proof
system either as rules or as axiom schemata.

	Note that the elimination of conditional terms may increase
the size of a sentence, because ⊗r occurs twice in the right
hand side of the above equivalence.  In the most unfavorable case,
⊗r is dominates the size of the expression so that writing it
twice almost doubles the size of the expression.

	Suppose that ⊗a and ⊗b in ⊗⊗qif_s_qthen_a_qelse_b⊗
are expressions that may contain the sentence ⊗s.  Occurrences
of ⊗s in ⊗a can be replaced by qtrue, and occurrences of ⊗s in
⊗b can be replaced by qfalse.  This follows from the fact that
⊗a is only evaluated if ⊗s is true and ⊗b is evaluated only
if ⊗s is false.

	This leads to a strengthened form of the law of replacement
of equals by equals.  The ordinary form of the law says that if
we have ⊗⊗e_=_e'⊗, then we can replace any occurrence of ⊗e in 
an expression by an occurrence of ⊗e'.  However, if we want
to replace ⊗e by ⊗e' within ⊗a within
⊗⊗qif_s_qthen_a_qelse_b⊗,
then we need only prove ⊗⊗s_⊃_e_=e'⊗, and to make the replacement
within ⊗b we need only prove ⊗⊗¬s_⊃_e_=_e'⊗.

	More facts about conditional terms are given in [McCarthy 1963]
including a discussion of canonical forms that parallels the canonical
forms of Boolean terms.  Any question of equivalence of conditional
terms is decidable by truth tables analogously to the decidability of
propositional sentences.
.ss(lambdarule,Lambda-expressions.)

	The only rule required for handling lambda-expressions
in first order logic is called ⊗lambda-conversion.  Essentially it is

⊗⊗⊗[λx: e][a] =⊗ < the result of substituting ⊗a for ⊗x in ⊗e >.

As examples of this rule, we have

⊗⊗⊗[λx: qa x . y][u . v] = [qa [u . v]] . y .		⊗

However, a complication requires modifying the rule.  Namely,
we can't substitute for a variable ⊗x an expression ⊗e that has a free variable
⊗y into a context in which ⊗y is bound.  Thus it would be
wrong to substitute ⊗⊗y_+_z⊗ for ⊗x in ⊗⊗∀y:_[x_+_y_=_z]⊗ or into
the term ⊗⊗[λy:_x_+_y][u_+_v]⊗.  Before doing the substitution, the
variable ⊗y would have to be replaced in all its bound occurrences by
a fresh variable.   In order to handle lambda expressions in our formal
proof system we would add a "reduction" rule which would derive a formula
⊗s' from a formula ⊗s where ⊗s' is the result of carrying out the above
substitutions (carefully) on some subexpression of ⊗s.  

	Lambda-expressions can always be eliminated from sentences and
terms by lambda-conversion, but the expression may increase greatly
in length if a lengthy term replaces a variable that occurs more than
once in ⊗e.  It is easy to make an expression of length proportional to ⊗n whose
length is proportional to 2%5n%* 
after conversion of its ⊗n nested lambda-expressions.
For example 

	
⊗⊗⊗λxq1: [xq1.xq1][ ... [λxq-: [xq-.xq-][$$A$]] ... ]⊗

becomes 

		$$(A . A)$,

		$$((A . A) . (A . A))$,

or
.begin nofill 

		$$((((A . A) . (A . A)) . ((A . A) . (A . A))) $
		$$  . ((A . A) . (A . A)) . ((A . A) . (A . A))))$
.end
for ⊗n = 1, 2, or 4 respectively.
.ss(funrule,Introducing facts about recursively defined functions.)

	The only remaining task in our development of a technique
for proving properties of LISP programs is to explain how to
extend the theory we have built so far to include axioms
characterizing such programs.  In this section we will explain
the connection between programs and functions.   In order to do this in a  
clean and uniform manner, we will restrict the class of programs to have a
particular form.   This doesn't really restrict our computing
power,  although it does limit the bag of tricks from which
we may choose when writing a program.  
We will then treat a special class of programs which "terminate on form".
Finally we describe the general form of program and show how
to prove that a program terminates.
We will postpone until a later section (qsect{subsection partfunrule})
discussing the characterization
of programs that do not terminate for all possible input values.   
In later chapters we will see how to extend our methods to larger classes
of programs and to properties that depend on the actual computation, not
just the value obtained.

	Suppose we have a recursive definition (program) of the form

!eqntau ⊗⊗⊗f[x]←qt[f,x]       ⊗

where qt is a suitably nice LISP term involving the variable ⊗x, the
function name ⊗f and perhaps other known functions and S-expression constants.
(The phrase "suitably nice" will be made more precise shortly.)  
Then using the rules for computation given in Chapter {SECTION READIN} 
we can show that there is a unique function, which we also call ⊗f, 
on the extended S-expressions such that
.begin indent 4,12

(i)  ⊗⊗f[x] = qt[f,x]⊗ for all S-expressions ⊗x.   

(ii)  ⊗f is the "least defined" such function.  That is, if ⊗g is any other 
function satisfying (i), then whenever ⊗f[x] is defined (eg. not qb) for an
S-expression ⊗x then ⊗g[x] is also defined and ⊗⊗f[x]_=_g[x]⊗.

(iii)  For any particular S-expression ⊗a, the value of
⊗f[a] is an S-expression (defined) if and only if the computation
prescribed by {eqn tau} terminates with that same value.
.end
Thus we see that if the computation defined by {eqn tau} always terminates
then there is only one solution to the corresponding functional equation
and that is precisely the function computed by the program.
Notice also that if we can prove that ⊗⊗issexp f[x]⊗  using the
functional equation and other facts about LISP, then we will have
shown that the computation prescribed by {eqn tau} terminates with a
well defined answer.
In any case there is a "distinguished" function that we associate with the 
program and we are allowed to add the new function symbol to our language, and
add to the set of axioms the functional equation corresponding to the definition.
The meaning of this new symbol will be the distinguished
function on extended S-expressions described above.


	In Chapter {SECTION WRITIN} we discussed various forms of recursive 
definitions.   Some these forms we claimed had the property that any program
fitting that form terminates for all allowed input.  We will not prove this 
statement, however the method we give below for proving that particular programs 
terminate can be used to justify the statement in the sense that using this 
method you could prove termination for any particular program that fits one
of these forms.   For reference we recall some of these forms for number, 
list and S-expression recursions.

!eqntau1 ⊗⊗⊗f[n,y] ← qif n=$0 qthen g[y] qelse h[n-$$1$,y,f[n-$$1$,j[n-$$1$,y]]]⊗.

!eqntau2 ⊗⊗⊗f[u,y] ← qif qn u qthen g[y] qelse h[qa u, qd u, y, f[qd u, j[qa u, qd u, y]]⊗.

!eqntau3 ⊗⊗⊗   f[x,y] ← qif qat x qthen g[x,y] qelse h[qa x,qd x,y,f[qa x,j1[qa x,qd x,y]],
f[qd x,j2[qa x,qd x,y]]]⊗

The symbols ⊗g, ⊗h, ⊗j, ⊗j1, ⊗j2 occuring in these definitions must be
functions expressions denoting
known functions  whose values are of the appropriate sort.  In particular
the ⊗⊗j⊗'s should return values matching the sort of the second argument
of ⊗f, and ⊗g and ⊗h should return values matching the sort of the last
argument of ⊗h.  The term "known function" means the expressions
involve only previously defined function, predicate and constant  symbols.
Programs of the above forms are in the category of "suitably nice"
Further, the value of the function computed by such a program
will be in the subdomain containing the values of ⊗g and ⊗h.  
(For readibility we have included just a single parameter ⊗y in each of the
above forms.  In general we allow any number of parameters (including none)
to appear, and they may be S-expression, list or number variables.)  

	Given a recursive definition having one of the above forms
we may add the function name to our language and the corresponding functional
equation (fully quantified) to our list of axioms.   Furthermore 
we may add an axiom stating that the value of ⊗f is in the subdomain  
which is the union of the possible values of ⊗g and ⊗h.  An example
should make this procedure clearer.

.cb Example

	Consider the recursive definitions of ⊗append, ⊗size, ⊗fringe and 
⊗length.  (We assume at this point that "+" and simple properties
of numbers are known and will mainly concentrate on techniques for proving
facts about functions on lists and S-expressions.)   


!fcnappend&4 ⊗⊗⊗u*v ← qif qn u qthen v qelse qa u . [qd u * v]⊗.

!fcnsize&2 ⊗⊗⊗size x ← qif qat x qthen $1 qelse size qa x + size qd x⊗,

!fcnfringe&3 ⊗⊗⊗fringe x ← qif qat x qthen <x> qelse fringe qa x * fringe qd x⊗,

!fcnltngth&h3 ⊗⊗⊗length u ← qif qn u qthen $0 qelse $$1$ + length qd u⊗

By the rules give above, since each of these definitions has one of
the forms {eqn tau2} or {eqn tau3}, we may add the following 
axioms to our theory:
.begin nofill turnon "∂"
.n←20

$APPEND: ∂(n)⊗⊗∀u v:[u*v = qif qn u qthen v qelse qa u . [qd u * v]]⊗
         ∂(n)⊗⊗∀u v: islist u*v ⊗

$SIZE:   ∂(n)⊗⊗∀x:[size x  = qif qat x qthen $1 qelse size qa x + size qd x]⊗
         ∂(n)⊗⊗∀x: numberp size x⊗

$FRINGE: ∂(n)⊗⊗∀x:[fringe x = qif qat x qthen <x> qelse fringe qa x * fringe qd x]⊗
         ∂(n)⊗⊗∀x: issexp fringe x⊗

$LENGTH: ∂(n)⊗⊗∀u:[length u = qif qn u qthen $0 qelse $$1$+length qd u]⊗
         ∂(n)⊗⊗∀u: numberp length u⊗
.end

	Now we can use these new axioms to prove some properties.  In particular
we shall prove

⊗⊗⊗∀x: length fringe x = size x.                 ⊗

Since the definitions of ⊗fringe and ⊗size are simple S-expression recursions, 
we will try using the simple S-expression induction schema, $SEXPINDUCTION, 
given in section qsect{subsection lispinduct}
to carry out the proof.  Thus we let qP be given by

⊗⊗⊗qP[x] ≡ [length fringe x = size x].           ⊗


	There are two cases to consider.  First if ⊗x is an atom then
we have
.begin nofill turnon "∂"
.l←8; m←16; n←36;

∂(l)⊗⊗length fringe x = length <x> ⊗  ∂(n) by $FRINGE 
	∂(m)⊗⊗= $$1$+length qd <x> ⊗  ∂(n) by $LENGTH, since ⊗⊗<x> = x . qnil⊗ is a non-null list.
	∂(m)⊗⊗= $$1$+length qnil ⊗  ∂(n) by $CDR-CONS 
	∂(m)⊗⊗= $1 ⊗ ∂(n) by $LENGTH and properties of +. 
	∂(m)⊗⊗= size x ⊗  ∂(n) by $SIZE 
.end
In the second case ⊗x is non-atomic and we have the induction hypothesis

⊗⊗⊗[length fringe qa x = size qa x] ∧ [length fringe qd x = size qd x]⊗

We begin by expanding the definitions of ⊗fringe and ⊗size to obtain
.begin nofill turnon "∂"
.l←8; m←12; n←50;

∂(l)⊗⊗length fringe x = length[fringe qa x * fringe qd x]⊗  ∂(n) by $FRINGE 
and
∂(l)⊗⊗size x = size qa x + size qd x ⊗ ∂(n) by $SIZE 
	∂(m)⊗⊗= [length fringe qa x] + [length fringe qd x]⊗ ∂(n) by the induction hypohesis
.end

Since ⊗⊗fringe qa x⊗ and ⊗⊗fringe qd x⊗  are lists 
(¬qat ⊗x means qa ⊗x and qd ⊗x are S-expressions so we may use the second of the
$FRINGE axioms)
we are reduced to proving something of the form ⊗⊗length[u*v]=length_u_+_length_v⊗.
This suggests that we prove a general lemma,  then the proof will be complete.
Thus we will prove

⊗⊗⊗∀u v:[length[u*v]=length u + length v].      ⊗ 

Since the definition of ⊗append is by recursion on ⊗u we will use  simple
list induction for the proof.
Again there are two cases. In the first case we have qn ⊗u and
.begin nofill turnon "∂"
.l←8; m←16; n←48;

∂(l)⊗⊗length[qnil*v] = length v ⊗  ∂(n) by $APPEND. 
	∂(m)⊗⊗= $0 + length v ⊗ ∂(n) by properties of $0 and "+".
	∂(m)⊗⊗= length qnil + length v ⊗ ∂(n) by $LENGTH. 
.end
In the second case we have ¬qn ⊗u and the induction hypothesis

⊗⊗⊗length [qd u]*v = length qd u + length v⊗.

thus
.begin nofill turnon "∂"
.l←8; m←16; n←48;

∂(l)⊗⊗length[u*v] = length[qa u . [qd u]*v]⊗ ∂(n) by $APPEND. 
	∂(m)⊗⊗= $$1$ + length [qd u]*v ⊗ ∂(n) by $LENGTH and $EQ-CONS. 
	∂(m)⊗⊗= $$1$ + [length qd u + length v]⊗ ∂(n) by induction hypothesis.
	∂(m)⊗⊗= length u + length v⊗ ∂(n) by associativity of + and $LENGTH.  
.end
this completes the proof of the lemma and thus of the original theorem.

	As we mentioned earlier, there are many programs that terminate
for all allowed input, but do not fit into one of the forms 
{eqn tau1} to {eqn tau3}.  We could give more general forms.
[A particularly nice example can be found in Boyer and Moore[1978]].
There are two reasons for not proceeding in this direction now.
One is that the more general forms are correspondingly more difficult
to recognize, the other is that in order to include the most general class of
programs we will eventually have to allow a recursive definitions
that are not necessarily total on form.  (This is a consequence of the
"halting problem" which we will say more about in Chapter_{SECTION COMPUT}.)  

	Our most general form of recursive definition in the category of 
"suitably nice" definitions has the following basic form

!eqngentau ⊗⊗⊗f[x1, ... xn] ← qt[f,x1, ... ,xn]⊗

where the term ⊗⊗qt[f,x1, ... ,xn]⊗ is formed like a term in our language
with the following restrictions.  No quantifiers appear.  The symbol qb
does not appear.  The function
symbols that appear must be those of the basic language, previously
recursively defined, or the symbol ⊗f.  The predicate symbols are
those of the basic language.  (We will relax this when we develop a
method of defining new predicates.)  Formulas appearing in the qif part
of a conditional are further restricted by not allowing ⊗f to appear
and further all terms that appear must denote S-expressions.  The point of 
these latter restrictions is mainly to avoid the possibility of having the qif
part of a conditional undefined.   If we think of the term qt as
arising from the constructs of our programming language the problem
with quantifiers does't arise, as we have no quantifiers.   However
it is convenient to be able to imbed the description in the language
of our theory as well.   We can further generalize the form
of definition by allowing mutually recursive definitions.  Thus
.begin nofill turnon "∂"
.n←24; m←32

∂(n)⊗⊗f1[x1, ... xn] ← qt1[f1, ... ,fm,x1, ... ,xn]⊗
∂(m).
!eqntautau ∂(m).
∂(m).
∂(n)⊗⊗fm[x1, ... xn] ← qtm[f1, ... ,fm,x1, ... ,xn]⊗
.end
is a "suitably nice" collection of definitions if the terms qt⊗i 
satisfy the restrictions above, allowing any the ⊗fi to appear
where ⊗f was allowed the single definition case.   We will see several
examples of mutually recursive definitions in later sections.

.cb Example 
	As a final example for this section we will prove that the alternate
definition, ⊗flatten, of ⊗fringe is "correct", namely that it computes the same 
function as ⊗fringe does.  This will demonstrate two more ideas.  First,
the definition is allowed by the general schema {eqn gentau}, but
it is not one of the forms {eqn tau1}, {eqn tau2}, or {eqn tau3}.
Thus we may introduce the appropriate functional equation(s) as
axioms in our theory, but we will have to prove that the value of the
defined function is always a list.   Second, the definition of ⊗flatten 
involves an auxiliary definition and more importantly this auxiliary 
definition uses an auxiliary variable, thus we will have to prove something
more general than we might have imagined in order for the induction step to work.
Recall the definitions
.begin nofill

⊗⊗⊗flatten[x] ← flat[x, qNIL]		⊗
!fcnflatten&3 
⊗⊗⊗flat[x,u] ← qif qat x qthen x.u qelse flat[qa x,flat[qd x,u]]⊗.
.end
We add to our theory the axioms
.begin turnon "∂"
.n←20

$FLATTEN: ∂(n)⊗⊗∀x:[flatten[x] = flat[x, qNIL]]⊗

$FLAT: ∂(n)⊗⊗∀x u:[flat[x,u] = qif qat x qthen x.u qelse flat[qa x,flat[qd x,u]]]⊗.
.end

First we will prove 

⊗⊗⊗∀x u: islist flat[x,u].              ⊗   

This tells us that the progam
for ⊗flat terminates for all input pairs ⊗[x,u] and further that the
term ⊗flat[x,u] may be used wherever a list is expected.
Since the definition is by simple S-expression recursion we use 
the simple S-expression induction schema for the proof.  
Again there are two cases.  In the case qat ⊗x we have
⊗⊗flat[x,u]_=_x_._u⊗ and by $CONS we have ⊗⊗islist flat[x,u]⊗.   In the
case ¬qat ⊗x, we have the induction hypothesis

⊗⊗⊗∀u: islist flat[qa x,u] ∧ ∀u: islist flat[qd x,u]⊗.

By $FLAT we have ⊗⊗flat[x,u] = flat[qa x,flat[qd x,u]]⊗. Using the 
qqd-part of the hypothesis we then can apply the qqa-part with ⊗u replaced
by ⊗⊗flat[qd x,u]⊗ and this completes the proof.  An immediate consequence
of this proof and $FLATTEN is that ⊗⊗∀x:_islist_flatten_x⊗.

	Now we will prove ⊗⊗∀x: flatten x = fringe x⊗.   By $FLATTEN this
is the same as ⊗⊗∀x:_flat[x,qnil]_=_fringe_x⊗.   The simple principles we
have used so far suggest that we proceed directly with a proof by S-expression
induction on ⊗x.  This unfortunately arrives at a dead end.  (The reader
is encouraged to try it and see.)  The difficulty is that we begin with
the second argument qnil, but after expanding the definition once this is
no longer the case.  Just as we have to carry along an extra variable in
the computation we also do in the proof.  There are several possible routes
to take.  We will prove the following more general statement

⊗⊗⊗∀x u: flat[x,u] = fringe x * u.            ⊗

Clearly the statement we started to prove is a direct consequence of this one.
Now we may proceed by simple S-expression induction.   In the case that
⊗x is an atom we have:
.begin nofill turnon "∂" group
.l←4;m←12;n←40;

∂(l)⊗⊗flat[x,u] = x . u⊗    ∂(n) by $FLAT 
          ∂(m)⊗⊗= <x> * u⊗  ∂(n) by $APPEND, since ⊗⊗<x> = x . qnil⊗.
          ∂(m)⊗⊗= fringe x * u⊗  ∂(n) by $FRINGE 
.end
In the case that ⊗x is non-atomic we have the induction hypothesis:

⊗⊗⊗∀u: flat[qa x,u]_=_fringe qa x * u ∧ ∀u: flat[qd x,u] = fringe_qd x * u⊗. 

and we have
.begin nofill turnon "∂" group
.l←4;m←12;n←40;

∂(l)⊗⊗flat[x,u] = flat[qa x,flat[qd x,u]]⊗  ∂(n) by $FLAT 
	    ∂(m)⊗⊗= flat[qa x,fringe qd x * u]⊗  ∂(n) by induction hypothesis
	    ∂(m)⊗⊗= fringe qa x * [fringe qd x * u]⊗ ∂(n) by induction hypothesis using ⊗⊗islist fringe qd x * u⊗
	    ∂(m)⊗⊗= fringe x * u⊗   ∂(n) by associativity of ⊗append, 
.end
This completes the proof.
Notice that in order to apply the induction hypothesis and the associativity
of ⊗append it is neseccary to know that 
⊗⊗islist fringe qd x ⊗ and ⊗⊗islist fringe qa x⊗.
.skip 2
.cb  Exercises
.item←0

#.  Review your proofs of properties of ⊗reverse from the exercises
of section qsect{subsection appendpf} to see that they do indeed fit into our 
formalism.

.group
#.  You were asked to write definitions for the function
⊗mirror in the exercises of Chapter {subSECTION WRITINex!}.  
Use the previously given definitions of ⊗fringe and ⊗reverse 
(and any facts proved about them so far) to show that your program
satisfies

⊗⊗⊗∀x:[reverse fringe x = fringe mirror x]⊗.

.apart
.ss(predrule,Recursively Defined Predicates.)

	In the last section we discussed how to introduce facts about
recursively defined functions into our theory of LISP.  We discovered
that for suitably nice recursive definitions we could translate the
definition directly into a first-order sentence by replacing "←" by "="
and quantifying over the formal parameters.
In Chapter {SECTION READIN} we introduced propositional constructs
⊗and, ⊗or and ⊗not into the programing language with the intent
that they should behave like the usual logical operators.  We even
represented these operators by the corresponding logical symbols
when describing programs by recursive definitions in external form.
We also treated some of the recursive definitions as though they
defined predicates rather than functions (for example ⊗member and ⊗equal).  
Thus we have expressions in external form such as
⊗⊗qif member[x,y] qthen ...⊗ rather than ⊗⊗qif member[x,y]≠qNIL qthen ... ⊗.

	How can we translate a recursive definition into a  first
order sentence that defines a predicate?   
Suppose we try just replacing "←" by "≡" in the
recursive definition.  Consider the following definition:

!fcnlose&  ⊗⊗⊗lose x ← ¬lose x ⊗.

This would translate into

!eqnloseax ⊗⊗⊗∀x:[lose x ≡ ¬lose x] ⊗.

which clearly loses!  We avoided a similiar problem for function definitions
by adding the element qb to the domain thus providing a non S-expression
value to assign to a term when the computation did not produce a value.
An analogous solution for predicates is possible.  Namely, we could
use a three valued logic where one of the values represents the
undefined element.   This makes reasoning in the logic unnecessarily
complicated as there are now have three cases instead of two when examining
possible truthvalues.   An alternate solution, which we will use, is
the following.  We continue to view recursive definitions
as defining functions.  Some of these functions will be intended
to represent predicates in the sense that the predicate is true 
only for those values of the arguments for which the function has
a non qNIL value.  

	For example consider the recursive program

!fcnsubexpf& ⊗⊗⊗subexpf[x, y] ← [x = y] ∨ [¬qat y ∧ [subexpf[x, qa y] ∨ subexpf[x, qd y]]]⊗.

Our intent is to define a predicate ⊗subexp satisfying the equivalence

!eqnsubexp ⊗⊗⊗∀x y: [subexp[x, y] ≡ [x = y] ∨ [¬qat y ∧ [subexp[x, qa y] ∨ subexp[x, qd y]]]]⊗.

First we must express the function definition as an allowed term.  We add primitive
functions ⊗iff, ⊗and, ⊗or, ⊗not, ⊗equal, ⊗atom, and ⊗null to our language and
axiomatize them to correspond to the LISP programs as described in 
Chapter {SECTION READIN}.  Then we can translate the recursive definition 
into a first order sentence as follows:

!eqnsubexpdef ⊗⊗⊗   ∀x y: subexpf[x, y] = [x equal y] or [not atom y and [subexpf[x, qa y] or subexpf[x, qd y]]]⊗

We can define the predicate ⊗subexp by

!eqnsubexp1 ⊗⊗⊗∀x y: [subexp[x, y] ≡ issexp subexpf[x, y] ∧ subexpf[x, y] ≠ qNIL]⊗.

Using this equation for ⊗subexpf and the S-expression induction axiom we can show

!eqnsubexpt ⊗⊗⊗∀x y: issexp subexpf[x, y].       ⊗

which is the statement that ⊗subexpf is total.  It then follows that

!eqnsubexp2 ⊗⊗⊗∀x y: [subexp[x, y] ≡ subexpf[x, y] ≠ qNIL]⊗.

and we can prove the original sentence proposed for ⊗subexp using
the definition and properties of the propositional functions.
We will sketch the proof after
giving the axioms for the newly introduced functions and stating
some useful consequences.

.bb Axioms for propositional functions.
.begin nofill turnon "∂"
.n←8

$IFF: 	∂(n)⊗⊗∀Z X Y: [iff[Z, X, Y] = qif ¬issexp Z qthen qb qelse qif [Z ≠ qNIL] 
qthen X qelse Y]⊗

$NOT:	∂(n)⊗⊗∀X: [not X = iff[X, qNIL, qT]]⊗

$AND:	∂(n)⊗⊗∀X Y: [X and Y = iff[X,Y,qNIL]]⊗

$OR: 	∂(n)⊗⊗∀X Y: [X or Y = iff[X, X, Y]]⊗

$EQUAL:	∂(n)⊗⊗∀X Y: [X equal Y] = qif [¬issexp X ∨ ¬issexp Y] qthen qb qelse qif [X = Y] qthen qT qelse qNIL]⊗

$ATOM:	∂(n)⊗⊗∀X: [atom X = qif [¬issexp X] qthen qb qelse qif qat X qthen qT qelse qNIL]⊗

$NULL:  ∂(n)⊗⊗∀X: [null X = qif [¬issexp X] qthen qb qelse qif qn X qthen qT qelse qNIL]⊗
.end
.bb Useful properties of propositional functions.
.begin nofill turnon "∂"
.n←20

$SEXPIFF:		∂(n)⊗⊗∀x y z:  issexp iff[x, y, z]⊗

$SEXPNOT: 		∂(n)⊗⊗∀x: issexp not x⊗

$SEXPAND: 		∂(n)⊗⊗∀x y: issexp [x and y]⊗

$SEXPOR:		∂(n)⊗⊗∀x y: issexp [x or y]⊗

$SEXPEQUAL: 		∂(n)⊗⊗∀x y: issexp [x equal y]⊗

$SEXPATOM:  		∂(n)⊗⊗∀x: issexp atom x⊗

$EQIFF:			∂(n)⊗⊗∀x y z: iff[x, y, z] = qif x ≠ qNIL qthen y qelse z⊗

$EQNOT:        		∂(n)⊗⊗∀x: [not x = qnil ≡ x ≠ qNIL]⊗

$EQAND: 		∂(n)⊗⊗∀x y: [x and y ≠ qNIL ≡ [x ≠ qNIL ∧ y ≠ qNIL]]⊗

$EQOR: 			∂(n)⊗⊗∀x y: [x or y ≠ qNIL ≡ [x ≠ qNIL ∨ y ≠ qNIL]]⊗

$EQEQUAL: 		∂(n)⊗⊗∀x y: [x equal y ≠ qNIL ≡ x = y]⊗
              		∂(n)⊗⊗∀x y: [x equal y = qT ≡ x = y]⊗

$EQATOM: 		∂(n)⊗⊗∀x: [atom x ≠ qNIL ≡ qat x]⊗
                  	∂(n)⊗⊗∀x: [atom x = qT ≡ qat x]⊗

$EQNULL: 		∂(n)⊗⊗∀x: [null x ≠ qNIL ≡ qn x]⊗
                  	∂(n)⊗⊗∀x: [null x = qT ≡ qn x]⊗
.end
The above facts follow directly from the defining axioms.  They essentially
express the fact that the propositional functons represent the logical
operations in the intended manner.  

	We remark that our method of interpreting functions as predicates
was chosen to correspond with the usual LISP convention.  Other
conventions are possible.  For example we could restrict the functions
that are to be interpreted as predicates to have values in the domain
α{qT, qNIL, qb}.  The axioms for qand etc. would be slightly different,
but not much else changes.  One difference is in the form of the
facts we can prove about the propostional operations.  In the latter case
we restrict our proofs to arguments ranging over the three element domain
and they will appear much like the standard facts about propositional operations.
Thus we could prove facts such as ⊗⊗not_not_x_=_x⊗ for all ⊗x in
the three element domain.  In our case this fact is also true for ⊗x 
in the three element domain, but not for more general ⊗x.  What we
can prove is the fact that for S-expressions ⊗x, ⊗⊗not_not_x_≠_qNIL_≡_x_≠_qNIL⊗.   
Other standard laws (such as de Morgan's laws) have similar analogues.

.cb Example: definition of ⊗subexp.  

	Now we can show that ⊗subexpf and ⊗subexp as defined by {eqn subexpdef}
and {eqn subexp1} have the desired properties.  First we prove that
⊗subexpf is total {eqn subexpt}.
Since the recursion in the definition of ⊗subexpf is on the second argument,
we will use the simple S-expression induction schema with

⊗⊗⊗qP[y] ≡ ∀z. issexp subexpf[z,y].              ⊗

In the case that ⊗y is an atom we have ⊗⊗not atom y = qNIL⊗ so the final ⊗and 
evaluates to qNIL.  Thus we can apply $SEXPEQUAL and $SEXPOR  to show that ⊗issexp 
holds in this case.  In the case that ⊗y is non-atomic we have the 
induction hypothesis

⊗⊗⊗issexp subexpf[x,qa y] %1and%* issexp subexpf[x,qd y].⊗

Thus we can use $SEXPEQUAL, $SEXPOR, and $SEXPAND to complete the proof.   As we
mentioned above {eqn subexp2} now follows from {eqn subexpt} and {eqn subexp1}.

	Now we can prove that ⊗subexp satisfies the equivalence that we intended
from the start.  The proof is just a sequence of simplifications based on the
use the $EQ- lemmas, the definitions and the totality of ⊗subexpf.  
We wish to prove
.begin nofill

⊗⊗⊗∀x y: [subexp[x, y] ≡ [x = y] ∨ [¬qat y ∧ [subexp[x, qa y] ∨ subexp[x, qd y]]]]⊗

which by {eqn subexp2} reduces to proving

⊗⊗⊗∀x y: [ [[x equal y] or [not atom y and [subexpf[x, qa y] or subexpf[x, qd y]]]]≠qNIL⊗
⊗⊗⊗        ≡ [x = y] ∨ [¬qat y ∧ [subexp[x, qa y] ∨ subexp[x, qd y]]] ]                     ⊗
.end

In the case that ⊗y is atomic the left-hand side reduces as before to

⊗⊗⊗ [[x equal y] or qNIL]≠qNIL⊗

which by $EQOR and $EQEQUAL reduces to ⊗⊗x=y⊗.  As ⊗⊗¬qat y⊗ is false the
right-hand side also reduces to ⊗⊗x=y⊗, so we are done with the atomic case.

In the case that ⊗y is non-atomic we have ⊗⊗issexp subexpf[x,qa y]⊗
and ⊗⊗issexp subexpf[x,qd y]⊗ thus we can apply $EQOR, $EQAND and $EQEQUAL 
to reduce the left-hand side to

⊗⊗⊗[x = y] ∨ [[not atom y]≠qNIL ∧ [subexpf[x, qa y]≠qNIL ∨ subexpf[x, qd y]≠qNIL]]⊗.

Finally we use $EQATOM and $EQNOT to replace ⊗⊗[not_atom_y]≠qNIL⊗ by 
⊗⊗¬qat y⊗ and {eqn subexp2} to finish the transformation of the left-hand side
to the expression on the right-hand side of the "≡".  This completes the proof.

.cb Exercise

	You were asked to write the definition for the predicate ⊗istail in the 
exercises of Chapter_{subSECTION WRITINex!}.  
Prove the following facts about ⊗istail.  
.begin nofill  indent 12,12

⊗⊗∀v: istail[qNIL,v]⊗
⊗⊗∀u v: [¬qn u ∧ istail[u,v] ⊃ istail[qd u,v]]⊗
⊗⊗∀u v w: [istail[u,v] ∧ istail[v,w] ⊃ istail[u,w]]⊗
.end

First translate your definition of ⊗istail into a functional equation for
the function ⊗istailf.  Show ⊗istailf is total and that ⊗istail satisfies
the equivalence you intended.  All of this parallels the ⊗subexp example
above.  For the rest you are on your own.


.ss(samefr,The SAMEFRINGE problem.)
 
	As a non trivial application of the techniques described in the previous
sections, we will give a proof of correctness of the predicate ⊗samefringe 
which has been proposed as a solution of the SAMEFRINGE problem.  This is the
problem of determining whether or not two S-expressions have the same fringe
using a minimum of space.  We will be concerned only with the correctness of
⊗samefringe since the efficiency is not an ⊗extensional property.  

	We have already studied two programs for computing the fringe of an
S-expression, namely ⊗fringe and ⊗flatten.   
The predicate ⊗samefringe is computed by the LISP program
.begin nofill

!fcnsamefringe&  ⊗⊗⊗samefringe[x, y] ← x = y ∨ [¬qat x ∧ ¬qat y ∧ same[gopher x, gopher y]]⊗

!fcnsame&  ⊗⊗⊗same[x, y] ← qa x = qa y ∧ samefringe[qd x, qd y]⊗

!fcngopher&  ⊗⊗⊗gopher x ← qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]⊗.
.end

We translate the definitions into  first order sentences characterizing the 
functions computed by these programs in the manner of the previous
section as follows
.begin nofill

!eqnsamefrf ⊗⊗⊗∀x y:[samefringef[x, y] = [x equal y] or                                  ⊗
            ⊗⊗⊗                 [[not atom x and not atom y] and samef[gopher x, gopher y]]]⊗

!eqnsamef  ⊗⊗⊗∀x y:[samef[x, y] = [qa x equal qa y] and samefringef[qd x, qd y]⊗

!eqngopherf ⊗⊗⊗∀x:[gopher x = qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]]⊗
.end
The predicates are defined by
.begin nofill

!eqnsamefrdef ⊗⊗⊗∀x y:[samefringe[x,y] ≡ issexp samefringef[x,y] ∧ samefringef[x,y]≠qNIL]⊗

!eqnsamedef ⊗⊗⊗∀x y: [same[x, y] ≡ issexp samef[x,y] ∧ samef[x,y]≠qNIL]⊗
.end

Now if we prove 

!eqnsamefrt ⊗⊗⊗∀x y: issexp samefringef[x,y] ⊗

then 

!eqnsamefrdef1 ⊗⊗⊗∀x y:[samefringe[x,y] ≡  samefringef[x,y]≠qNIL]⊗

follows immediately using {eqn samefrdef} and
it is easy to show (as we did for ⊗subexp) that 

!eqnsamefr1 ⊗⊗⊗∀x y:[samefringe[x,y] ≡ x = y ∨ [¬qat x ∧ ¬qat y ∧ same[gopher x, gopher y]]⊗

	The correctness of ⊗samefringe can now be expressed by the statement

!eqnsamefrcor ⊗⊗⊗∀x y:[samefringe[x,y] ≡ fringe x = fringe y]⊗.

Recall the following axioms for ⊗fringe 
.begin nofill turnon "∂"
.n←16

$FRINGE:	∂(n)⊗⊗∀x: [fringe x = qif qat x qthen <x> qelse [fringe qa x] * [fringe qd x]]⊗
    		∂(n)⊗⊗∀x:_islist_fringe_x⊗.
.end

	Due to the complicated form of the recursion defining ⊗samefringe, simple
S-expression induction is not adequate to prove the above theorems.  Therefore 
we must be somewhat more clever and devise an induction
appropriate for the problem.  One way is to use induction
on the size of the S-expressions involved.  We recall the axioms for size
given in section qsect{subsection funrule}.
.begin nofill turnon "∂"
.n←16

$SIZE: 	∂(n)⊗⊗∀x: [size x = qif qat x qthen 1 qelse size qa x + size qd x]⊗
	∂(n)⊗⊗∀x: numberp size x⊗.
.end

⊗size provides a mapping of S-expressions into the domain of natural numbers
and allows us to transform the problem into one of natural number induction.
Namely, we will prove 

!eqnsamefrpf ⊗⊗⊗∀n: ∀x y: [[size x + size y] = n ⊃ $$THM$[x, y]]⊗

using the induction schema $NUMINDUCTION-CVI.  Here
$THM is the statement of totality {eqn samefrt} or of correctness
{eqn samefrcor}.   To complete the proof of $THM 
we instantiate {eqn samefrpf} by letting ⊗⊗n=size_x_+_size_y⊗ and obtain

⊗⊗⊗∀x y: $$THM$[x, y] .		⊗

	Now we proceed with the proof.  In addition to the lemmas  about
⊗append and the lemmas proved in the last section about the
propositional functions, we will need some lemmas
about ⊗gopher, ⊗fringe, ⊗size and combinations thereof. They are

$GOOD-GOPHER: 	⊗⊗∀x: [¬qat x ⊃ [issexp gopher x ∧ issexp qa gopher x ∧ issexp qd gopher x]]⊗

$FRINGE-ATM:	⊗⊗∀x y: [[qat x ∨ qat y] ⊃ [fringe x = fringe y ≡ x = y]]⊗

$FRINGE-GOPHER:	⊗⊗∀x: [¬qat x ⊃ [qa fringe x = qa gopher x] ∧ [qd fringe x = fringe qd gopher x]]⊗

$SIZE-GOPHER:	⊗⊗∀x y: [[¬qat x ∧ ¬qat y] ⊃ [size qd gopher x +size qd gopher y] 
< [size x + size y]]⊗

The first two are just bookkeeping and computational lemmas to fill in some 
details.  The $FRINGE-GOPHER lemma is really the key to why this program for
⊗samefringe works.  There are several proofs of the correctness of ⊗samefringe 
based on various inductions, but they all use this lemma.  The $SIZE-GOPHER 
lemma is what allows us to apply the induction hypothesis at the appropriate time.

	We will give only a brief indication of the proof of these lemmas.
The key idea in proving things about
⊗gopher is to first prove properties of ⊗⊗gopher[x_._y]⊗ as gopher is only
defined for non-atoms and every non-atom can be expressed as ⊗⊗x_._y⊗ for suitable
⊗x and ⊗y. For this purpose we start with some useful facts derived from $GOPHER, 
$FRINGE, $SIZE and the LISP axioms.

$GOPHER-CONS-ATM:	⊗⊗∀x y: [qat x ⊃ gopher[x . y] = [x . y]]⊗

$GOPHER-CONS-NOTATM:	⊗⊗∀x y: [¬qat x ⊃ gopher[x . y] = gopher[qa x. [qd x . y]]]⊗

$FRINGE-CONS:		⊗⊗∀x y: [fringe[x . y] = fringe x * fringe y]⊗

$SIZE-CONS:		⊗⊗∀x y:  [size[x . y] = size x + size y]⊗

	To prove $GOOD-GOPHER first prove, by a straight forward use of 
$SEXPINDUCTION on ⊗x, that

		⊗⊗∀x y: [issexp gopher[x . y] ∧ ¬qat gopher[x . y]]⊗

The lemma then follows from the LISP axioms. 

	For $FRINGE-ATM we assume ⊗⊗qat x⊗ and show by computation and 
using the algebraic facts about S-expressions that ⊗⊗fringe_x_=_fringe_y_≡_x_=_y⊗.
The lemma then follows from the symmetry of the occurrences of ⊗x and ⊗y.  
In particular, from the
definition of ⊗fringe we have ⊗⊗fringe_x_=_<x>_=_[x_._qNIL]⊗.  If ⊗⊗qqat_y⊗ the
result follows using $EQ-SEXP.  If ⊗⊗¬qat y⊗ then ⊗⊗x_≠_y⊗ and 
by the LISP axiom $EQ-SEXP we need only
prove ⊗⊗¬qn qd fringe y⊗. But this follows from properties of ⊗append. 

	To prove $FRINGE-GOPHER we use the "gopher trick" again and first prove

⊗⊗⊗∀x y: [qa fringe[x . y] = qa gopher[x . y] ∧ qd fringe[x . y] = fringe qd gopher[x . y]]⊗

using simple S-expression induction.  By properties of ⊗append  
and $FRINGE-CONS  
we have

⊗⊗⊗qa fringe[x . y] = qa fringe x,		⊗

and

⊗⊗⊗qd fringe[x . y] = [qd fringe x] * fringe y.	⊗

In the case ⊗⊗qat x⊗  the result follows from the facts that qNIL is a
left identity for ⊗append, $GOPHER-CONS-ATM, and ⊗⊗fringe_x_=_[x_._qNIL]⊗ .  
In the case ⊗⊗¬qat x⊗ we show

⊗⊗⊗fringe[x . y] = fringe[qa x . [qd x . y]]	⊗

using properties of ⊗append and $FRINGE-CONS.  Then the result follows from the
induction hypothesis and $GOPHER-CONS-NOTATM. 
$FRINGE-GOPHER now follows from the above using $CONS.  

To prove $SIZE-GOPHER we first show

⊗⊗⊗∀x y: [size qd gopher[x . y] < size[x . y]]⊗

using simple S-expression induction.  In the case ⊗⊗qat x⊗ we have 

⊗⊗⊗size qd gopher[x . y] = size y⊗  and  ⊗⊗size[x . y] = 1 + size y⊗

by $SIZE, $SIZE-CONS and $GOPHER-CONS-ATM and the result follows by properties
of numbers.  In the case ⊗⊗¬qat x⊗ we show 

⊗⊗⊗size[x . y] = size[qa x . [qd x . y]]⊗

using $SIZE-CONS, properties of numbers and the LISP axioms. The result then 
follows from the induction hypothesis and $GOPHER-CONS-NOTATM.  
$SIZE-GOPHER now follows from $CONS and properties of numbers.

	Now we are ready to begin the proof of the totality and correctness
of ⊗samefringe.  Since the form of the proofs
of {eqn samefrt} and {eqn samefrcor} are similar we will do the proofs "in
parallel".  That is we will prove ⊗⊗∀x y:$$THM$[x,y]⊗ where $THM is either
⊗⊗issexp_samefrf[x,y]⊗  or ⊗⊗samefringe[x,y]≡fringe_x=fringe_y⊗.  (We in fact use
the first theorem to prove the second, but not visa versa, so the argument
isn't cyclic.  We could just a easily do them separately, it would just be
somewhat repetative.)

	Recall that we are going to do a "course of values" induction
on the sum of the sizes of the arguments.  As is usual, the proof is divided 
into two cases, one in which the result follows by a fairly direct computation
and the second in which we are able to reduce the problem to a smaller 
case and make use of the induction hypothesis.
In the first case we assume ⊗⊗qat x ∨ qat y⊗.  Then by the propositional axioms 

⊗⊗⊗not atom x and not atom y = qNIL⊗,

and hence

⊗⊗⊗samefringef[x, y] = x equal y⊗.

Thus ⊗⊗issexp samefringef[x,y]⊗ follows from $SEXPEQUAL.   Further

⊗⊗⊗samefringe[x,y] ≡ [x equal y]≠qNIL ≡ x = y⊗

by {eqn samefrdef1} $EQEXPEQUAL and ⊗⊗samefringe[x,y]≡fringe_x=fringe_y⊗ follows
from $FRINGE-ATM.  

	In the second case we assume ⊗⊗¬qat x ∧ ¬qat y⊗ and make use of the
induction schema as discussed above.  In particular we have the induction hypothesis

⊗⊗⊗∀m: [m < n ⊃ ∀xq1 yq1: [size xq1 + size yq1 = m ⊃ $$THM$[xq1, yq1]] ⊗.

Taking  ⊗⊗n = size x + size y⊗, ⊗⊗m = size qd gopher x + size qd gopher y⊗,
⊗⊗xq1_=_qd gopher_x⊗ and ⊗⊗yq1_=_qd gopher_y⊗ we have by $SIZE-GOPHER 

⊗⊗⊗$$THM$[qd gopher x, qd gopher y]⊗

for either theorem that we are proving.
Assigning these values to ⊗n and ⊗m is allowed since  + and ⊗size 
return numbers and $GOOD-GOPHER says the argments to ⊗size are S-expressions.

	Using the axioms {eqn samefrf} and {eqn samef} we expand ⊗samefringef[x,y] 
and obtain
.begin nofill turnon "∂"
.n←4;m←21;

∂(n)⊗⊗[samefringef[x, y] = ∂(m)[x equal y] or [[not atom x and not atom y] ⊗
		∂(m+12)⊗⊗and [qa gopher x equal qa gopher y] ⊗
		∂(m+12)⊗⊗and samefringef[qd gopher x, qd gopher y]⊗
.end
⊗⊗issexp samefringef[x,y]⊗ is immediate from the $SEXP- propositional
axioms, $GOOD-GOPHER 
and the induction hypothesis.  By {eqn samefrdef1} we need only show that

.begin nofill turnon "∂"
.n←4;m←22;

∂(n)⊗⊗fringe x = fringe y ≡ ∂(m)[[x equal y] or [[not atom x and not atom y] ⊗
		∂(m+12)⊗⊗and [qa gopher x equal qa gopher y] ⊗
		∂(m+12)⊗⊗and samefringef[qd gopher x, qd gopher y]]≠qNIL⊗

.end
to prove the correctness version of $THM.  Since the arguments to the propositional
functions are all S-expressions we apply the $EQ- propositional
axioms and {eqn samefrdef1} to reduce to
.begin nofill turnon "∂"
.n←4;m←8;

∂(n)⊗⊗fringe x = fringe y ≡⊗
∂(m)⊗⊗x = y ∨ [[¬qat x ∧ ¬qat y] ∧ [qa gopher x = qa gopher y] ∧ samefringe[qd gopher x, qd gopher y]]⊗

.end
Using the induction hypothesis and simplifying the ⊗⊗¬qat x_∧_¬qat y⊗ to qtrue
we need only show
.begin nofill turnon "∂"
.n←4;m←12;

∂(n)⊗⊗fringe x = fringe y ≡⊗
∂(m)⊗⊗x = y ∨ [[qa gopher x = qa gopher y] ∧ fringe[qd gopher x]=fringe[qd gopher y]]⊗
.end

which follows easily from $FRINGE-GOPHER.  This completes the proof.


	In the above proof we could have equally well used the predicate

⊗⊗⊗qP n ≡ ∀x y: [size x = n ⊃ THM[x, y]]⊗

since the recursive call to ⊗samefringe always reduces the size of the first
argument.

	Another version of ⊗samefringe without any auxiliary functions is

.begin nofill turnon "∂" group
.n←16

∂(n)⊗⊗samefringe[x, y] ← ⊗
∂(n)⊗⊗    x = y ∨ ⊗
∂(n)⊗⊗    [¬qat x ∧ ¬qat y ∧ ⊗
!fcnsamefringe&1  ∂(n)⊗⊗        [qif qat qa x qthen [qif qat qa y qthen qa x = qa y ∧ samefringe[qd x, qd y] ⊗
∂(n)⊗⊗                             qelse samefringe[x, qaa y. [qda y . qd y]]]⊗
∂(n)⊗⊗         qelse samefringe[qaa x . [qda x . qd x], y]. ⊗
.end

Note that a recursive call to ⊗samefringe does one of the following three things:
.begin nofill

	1)  decreases  ⊗⊗size x + size y⊗
	2)  leaves  ⊗⊗size x + size y⊗ and ⊗⊗size qa x⊗ invariant and decreases ⊗⊗size qa y⊗
	3)  leaves  ⊗⊗sixe x + size y⊗ and ⊗⊗size qa y⊗ invariant and decreases ⊗⊗size qa x ⊗.
.end
.TURN ON "↑[]"
This can lead to a choice of an induction axiom schema in at least two ways.
If in the $NUMINDUCTION-CVI schema we let ⊗n and ⊗m range over all ordinals less
than a given one it becomes a schema of transfinite induction. Ordinary induction
is obtained as a special case where the bounding ordinal is qW the least transfinite
ordinal.  If we take the bounding ordinal to be qW↑[qW] then the SAMEFRINGE theorem
for the above version of ⊗samefringe can be proved using the predicate
.TURN OFF

⊗⊗⊗qP n  ≡ ∀x y: [[size x +size y]qW + size qa x + size qa y = n ⊃ $$THM$[x, y]]⊗


	Alternately one could axiomatize the lexicographic ordering of triples
of numbers by
.NOFILL

⊗⊗⊗∀l%41%* m%41%* n%41%* l m n: [(l%41%*, m%41%*, n%41%*) < (l, m, n) ≡				⊗
⊗⊗⊗[l%41%* < l] ∨ [l%41%* = l ∧ m%41%* < m] ∨ [l%41%* = l ∧ m%41%* = m ∧ n%41%* < n]]⊗
.FILL
This ordering is well-founded (has no infinite decreasing sequences) and so we
have a schema analogous to $NUMINDUCTION-CVI given by
.NOFILL

⊗⊗⊗∀l m n: [∀l%41%* m%41%* n%41%*: [(l%41%*, m%41%*, n%41%*) < (l, m, n) ⊃qP(l%41%*, m%41%*, n%41%*)] ⊃ qP(l, m, n)]⊗
⊗⊗⊗⊃ ∀l m n: qP(l, m, n)⊗
.FILL
The SAMEFRINGE theorems can now be proved using this schema with the predicate

⊗⊗⊗qP(l, m, n) ≡ ∀x y: [l = size x +size y ∧ m = size qa y ∧ n = size qa x ⊃ $$THM$[x, y]]⊗
.ss(partitionpf,Correctness of a Program to Partition Lists.)

	As a second non trivial example 
we consider a program that computes all of the partitions
of a list into a given number of sublists.   For a list ⊗w to be a partition
of a list ⊗u into ⊗n parts, ⊗w must be a list of ⊗n non-empty lists such
that ⊗⊗append⊗ing the elements of ⊗w together gives ⊗u.
Thus $$((A_B)_(C_D))$ is a 2-partition of $$(A_B_C_D)$ and

⊗⊗⊗partition[$$(A B C D), 2$] = $$(((A) (B C D)) ((A B) (C D)) ((A B C) (D)))$⊗.

The definition of partition is
.begin nofill turnon "∂" group
.n←16

∂(n)⊗⊗partition[u, n] ← ⊗
∂(n+4)⊗⊗qif n = $0 qthen $$ERROR$⊗
!fcnpartition& ∂(n+4)⊗⊗qelse qif n > length u qthen $$ERROR$⊗
∂(n+4)⊗⊗qelse qif n = $1 qthen <<u>>⊗
∂(n+4)⊗⊗qelse partn[<qa u>, qd u, n-$$1$]⊗
.apart
where
.group
∂(n)⊗⊗partn[u, v, n] ← ⊗
∂(n+4)⊗⊗qif n > length v qthen qNIL⊗
!fcnpartn& ∂(n+4)⊗⊗qelse qif n = $0 qthen qNIL⊗
∂(n+4)⊗⊗qelse qif n = 1 qthen [tack[u, <<v>>] * partn[u * <qa v>, qd v, n]]⊗
∂(n+4)⊗⊗qelse tack[u, partn[<qa v>, qd v, n-$$1$]]⊗
∂(n+8)⊗⊗* partn[u * <qa v>, qd v, n]⊗
.apart
and

!fcntack&1 ∂(n)⊗⊗tack[x, w] ← qif qn w qthen qNIL qelse [x . qa w] . tack[x, qd w]⊗

.end

Notice that we can only partition a list into ⊗n parts if the length of the
list is at least ⊗n, also it makes no sense to partition
a list into $0 parts.   ⊗partition works by considering all possible
"heads" of ⊗u as the first element of the partition and paritioning
the rest of ⊗u into one fewer parts.  The arguments to ⊗partn are
the current head, rest and numbers of parts to partition the rest into.

These definitions translate into first order sentences as follows:
.begin nofill turnon "∂" group
.n←12

∂(n)⊗⊗∀u n:[partition[u, n] = ⊗
∂(n+8)⊗⊗qif n = $0 qthen $$ERROR$⊗
!eqnpartitioneqn ∂(n+8)⊗⊗qelse qif n > length u qthen $$ERROR$⊗
∂(n+8)⊗⊗qelse qif n = $1 qthen <<u>>⊗
∂(n+8)⊗⊗qelse partn[<qa u>, qd u, n-$$1$]]⊗
.apart

.group
∂(n)⊗⊗∀u v n:[partn[u, v, n] = ⊗
∂(n+8)⊗⊗qif n > length v qthen qNIL⊗
!eqnpartneqn ∂(n+8)⊗⊗qelse qif n = $0 qthen qNIL⊗
∂(n+8)⊗⊗qelse qif n = 1 qthen [tack[u, <<v>>] * partn[u * <qa v>, qd v, n]]⊗
∂(n+8)⊗⊗qelse tack[u, partn[<qa v>, qd v, n-$$1$]]⊗
∂(n+12)⊗⊗* partn[u * <qa v>, qd v, n]]⊗
.apart

!eqntackeqn ∂(n)⊗⊗∀x w:[tack[x, w] = qif qn w qthen qNIL qelse [x . qa w] . tack[x, qd w]]⊗

.end

We also have 
.begin nofill turnon "∂" group
.n←16

!eqnpartitionlis ∂(n)⊗⊗∀u n:[length u > n > 0 ⊃ islist partition[u,n]]⊗
!eqnpartnlis ∂(n)⊗⊗∀u v n:islist partn[u,v,n]⊗
!eqntacklis ∂(n)⊗⊗∀x w:islist tack[x,w]⊗

.end

as {eqn tacklis} follows from the form of the defintion, {eqn partnlis}
follows by an easy list induction on ⊗v and {eqn partitionlis} then
follows from {eqn partnlis}.

We wish to prove that ⊗partition is correct according to some reasonable
criterion.   That is we would like to show that every partition of
⊗u into ⊗n parts is a member of the list ⊗partition[u,n] and
that every member of ⊗partition[u,n] is a partition of ⊗u into ⊗n parts
(assuming  ⊗u can be partitioned into ⊗n parts).  Thus we must
formalize what it means for a list ⊗w to be partition of ⊗u into ⊗ parts.
Let ⊗ispartition[u,w,n] express this fact.  Then the statement we
wish to prove is 

!eqnpartthm ⊗⊗⊗∀u w n:[length u ≥ n > $0 ⊃ [wεpartition[u,n] ≡ ispartition[u,w,n]] ]⊗ .

We can formalize our discussion at the beginning of this section as to what
it means to be a partition of a given list as follows:

!eqnispartitioneqv ⊗⊗⊗∀v w n:[ispartition[v, w, n] ≡ length w = n ∧ listlist w ∧ combine w = v]⊗.

where

!eqnlistlist ⊗⊗⊗∀u:[listlist u ≡ qn u ∨ [plistp qa u ∧ listlist qd u]]⊗

!eqnplistp ⊗⊗⊗∀x:[plistp x ≡ ¬qn x ∧ islist x]⊗

!eqncombineeqn ⊗⊗⊗∀w:[combine w = qif qn w qthen qNIL qelse qa w * combine qd w]⊗

⊗listlist_u expresses the fact that  ⊗u is a list of non-empty lists.
That it is consistent to add such axioms to our theory is a straighforward 
application of the methods of sections qsect{subsection funrule} and
qsect{subsection predrule} and we will not give the details.

	There is a second aspect to the correctness of ⊗partition, namely that
each partition occurs only once in the answer, e.g.

!eqnpartone ⊗⊗⊗∀u w n:[length u ≥n > $0 ⊃ multiplicity[w,partition[u,n]] ≤ $$1$]⊗

where ⊗multiplicity[x,u] is the number of occurrences of ⊗x in the list ⊗u.  
We will prove only {eqn partthm}, and leave {eqn partone} as an exercise.

	Thus we will proceed with our proof of {eqn partthm}.   First
note that using the definition of ⊗member given by ({eqn member!!}) we may define
the relation "ε" and show (using the method of qsect{subsection predrule})
that it satisfies the equivalence

!eqnmembereqv ⊗⊗⊗∀x u: [x ε u ≡ ¬qn u ∧ [x = qa u ∨ x ε qd u] ]⊗.

We recall the axioms for the defintion of ⊗length  

.begin nofill turnon "∂"
.n←16

$LENGTH:  ∂(n)⊗⊗∀u:[length u = qif qn u qthen $0 qelse $$1$+length qd u]⊗
         ∂(n)⊗⊗∀u: numberp length u⊗
.end

	The following lemmas are easy to prove (either by direct 
computation or simple induction) and will be left as exercises.

.begin nofill turnon "∂"
.n←16

!eqnpartlem0 ∂(n)⊗⊗∀w:[length w = $1 ∧ listlist w ⊃ combine w = qa w]⊗

!eqnpartlem1 ∂(n)⊗⊗∀w u v:[w ε u*v ≡ w ε u ∨ w ε v]⊗

!eqnpartlem2 ∂(n)⊗⊗∀w x v:[w ε tack[x,v] ≡ ∃w1:[w1 ε v ∧ w = x . w1]]⊗
.<<!partlem2 ∂(n)⊗⊗∀w x v:[w ε tack[x,v]≡qa w =x  ∧ qd w ε v]]⊗>>

!eqnpartlem3 ∂(n)⊗⊗∀u v:[¬qn u ⊃ ∀w:[w ε v ⊃ listlist w] ⊃ ∀w:[w ε tack[u,v] ⊃ listlist w]]⊗

!eqnpartlem4 ∂(n)⊗⊗∀v w:[length w > 1 ∧ listlist w ∧ combine w = v ⊗
     ∂(n+4)⊗⊗⊃ ∃v1:[qa w = <qa v>*v1 ∧ qd v = v1*[combine qd w]]]⊗

.end

To prove {eqn partthm} we assume that ⊗u and n⊗ satisfy ⊗⊗length_u_≥_n_≥_$$1$⊗
and show that

!eqnpartthm1 ⊗⊗⊗∀w:[wεpartition[u,n] ≡ ispartition[u,w,n] ]⊗ .

We consider two cases ⊗⊗n=$$1$⊗ and ⊗⊗n>$$1$⊗.  In the case that ⊗⊗n=$$1$⊗
we have 
.begin nofill turnon "∂"
.n←8 ;m←48

∂(n)⊗⊗partition[u,n] = <<u>> ⊗∂(m) by {eqn partitioneqn}
∂(n)⊗⊗w ε <<u>> ≡ w= <u>⊗  ∂(m) by {eqn membereqv}

thus ⊗⊗w ε partition[u,n]⊗ gives

∂(n)⊗⊗length w = $1 ⊗ ∂(m) by $LENGTH 
∂(n)⊗⊗listlist w  ⊗ ∂(m) by {eqn listlist} since by hypothesis ⊗plistp_u  
∂(n)⊗⊗combine w = u⊗ ∂(m) by {eqn combineeqn} and properties of ⊗append 

.end

which is equivalent to ⊗⊗ispartition[u,w,$$1$]⊗, and conversely
if ⊗⊗ispartition[u,w,$$1$]⊗ then using {eqn partlem0} we get ⊗⊗u=qa w⊗
or ⊗w=<u>, which completes the proof when ⊗n is $1.  

	In the case that ⊗n is greater than $1 we have
⊗⊗partition[u,n]=partn[<qa u>,qd u,n-$$1$]⊗ and the appropriate thing to
do is to prove a theorem about ⊗partn which applied to this particular 
case will give us the desired result.  We might try 

⊗⊗⊗∀u v w n:[¬qn u ∧ length v ≥ n ≥ $1 ⊃ [w ε partn[u,v,n] ≡ ispartition[u*v,w,n+$$1$]]⊗ .

It would indeed give us the proof that we wish, however it is not true.  The 
reason is that ⊗partn produces only those partitions in which the
first element is an extension of the argument ⊗u, and this condition
must be added to the right hand side of the equivalence before we
have a true theorem.  Thus we wish to show the following
.begin nofill

!eqnpartthm2 ⊗⊗⊗∀u v w m:[¬qn u ∧ length v ≥ m ≥ $1 ⊃ [w ε partn[u,v,m] ≡ ispartn[u,v,w,m]]⊗ .

where

!eqnispartneqv ⊗⊗⊗∀u v w m:[ispartn[u, v, w, m] ≡ ispartition[u*v,w,m+$$1$] ∧ ishead[u,v,w]⊗

and

!eqnisheadeqv ⊗⊗⊗∀u v w:[ishead[u,v,w] ≡ ∃u1:[u*u1=qa w ∧ u1*combine[qd w]=v]]⊗
.end

This we will prove by an induction on ⊗v.   As above we will assume that 
⊗⊗length_v_≥_m_≥$$1$⊗ and ⊗⊗¬qn u⊗ and show that

!eqnpartthm3 ⊗⊗⊗∀w:[w ε partn[u,v,m] ≡ ispartn[u,v,w,m]]⊗ .

First we will prove the forward implication.  Thus we assume ⊗⊗wεpartn[u,v,m]⊗
and show that ⊗⊗ispartn[u,v,w,m]⊗ holds.   
In the case that ⊗⊗m=$$1$⊗ we have

⊗⊗⊗partn[u,v,m]=tack[u, <<v>>] * partn[u * <qa v>, qd v, m]]⊗ .

As ⊗tack and ⊗partn produce lists we may use lemma {eqn partlem1} and thus 
reduce to one of the cases ⊗⊗wεtack[u,<<v>>]⊗ and ⊗⊗wεpartn[u*<qa v>,qd v,m]⊗.
In the first case we have 
.begin nofill turnon "∂"
.n←8 ;m←48

∂(n)⊗⊗w=<u_v>⊗ ∂(m) by {eqn tackeqn} and {eqn membereqv}
∂(n)⊗⊗length w = $2 ⊗ ∂(m) by $LENGTH  
∂(n)⊗⊗listlist w  ⊗ ∂(m) by {eqn listlist} since by
∂(m)  hypothesis ⊗plistp_u  and ⊗plistp_v 
∂(n)⊗⊗combine w = u*v⊗ ∂(m) by {eqn combineeqn} and properties of ⊗append 
∂(n)⊗⊗u*qNIL=qa w ∧ qNIL*combine qd w=v⊗ ∂(m) by {eqn combineeqn} and properties of ⊗append 
.end

and ⊗⊗ispartn[u,v,w,$$1$]⊗ follows.  In the second case 
⊗⊗wεpartn[u*<qa v>,qd v,$$1$]⊗ implies that the result is not qNIL and 
hence ⊗⊗length qd v_≥_$$1$⊗, so we may apply the induction hypothesis which 
says that
.begin nofill turnon "∂"
.n←8; m←48

∂(n)⊗⊗w ε partn[u*<qa v>,qd v,$$1$] ≡ ispartn[u*<qa v>,qd v,w,$$1$]⊗
∂(m)by induction
thus
∂(n+4)⊗⊗≡ispartition[[u*<qa v>]*qd v,w,$$2$] ∧ ∃u1:[[u*≤qa v>]*u1]=qa w ∧ u1*combine[qd w]=qd v]⊗
∂(m)by {eqn ispartneqv}
∂(n+4)⊗⊗≡ ispartition[u*v,w,$$2$] ∧ ∃u2:[[u*u2]=qa w ∧ u2*combine[qd w]= v]⊗
∂(m)by {eqn ispartitioneqv} using ⊗⊗u2=<qa v>*u1⊗
∂(n+4)⊗⊗≡ ispartn[u,v,w,$$1$]⊗∂(m)by {eqn ispartneqv}
.end

In the case ⊗⊗m>$$1$⊗ we have

⊗⊗⊗partn[u,v,m]=tack[u, partn[<qa v>, qd v, m-$$1$]] * partn[u * <qa v>, qd v, m]⊗ 

from {eqn partneqn}.  Again we have the two cases
⊗⊗wεtack[u,partn[<qa v>,qd v,m-$$1$]]⊗ or ⊗⊗wεpartn[u*<qa v>,qd v,m]⊗ .
Suppose ⊗⊗wεtack[u,partn[<qa v>,qd v,m-$$1$]]⊗, then ⊗⊗w=u_._w1⊗
where ⊗⊗w1εpartn[<qa v>,qd v,m-$$1$]⊗ by {eqn partlem2}.
By induction we have ⊗⊗ispartn[<qa v>,qd v,w1,m-$$1$]⊗ and thus
⊗⊗ispartition[v,w1,m]⊗.  Taking ⊗u2 as qNIL and using ⊗⊗w=u_._w1⊗
we get

⊗⊗⊗ispartition[u*v,w,m+$$1$] ∧ ∃u2: [[u*u2]=qa w ∧ u2*combine[qd w]= v]⊗

thus  proving ⊗⊗ispartn[u,v,w,m]⊗ as desired.
In the case that ⊗⊗wεpartn[u*<qa v>,qd v,m]⊗ the fact that ⊗⊗ispartn[u,v,w,m]⊗
follows by induction as in the case ⊗⊗m=$$1$⊗

To prove the backward implication we assume ⊗⊗ispartn[u,v,w,m]⊗
Thus ⊗⊗listlist_w⊗, ⊗⊗length_w_=_m+$$1$⊗, ⊗⊗combine_w_=u*v⊗,
⊗⊗u*u1=qa w⊗ and ⊗⊗u1*combine_qd w_=_v⊗ for some list ⊗u1.  
Now there are two cases depending on whether or not ⊗u1 is qNIL.

	If ⊗⊗u1=qNIL⊗ then ⊗⊗u=qa w⊗ and ⊗⊗v_=_combine_qd w⊗.  In the
case ⊗⊗m=$$1$⊗ we see that ⊗⊗w=<u v>⊗ and thus is in ⊗⊗partn[u,v,m]⊗
(recall the forward argument for the case ⊗⊗m=$$1$⊗).
If ⊗⊗m>$$1$⊗ then we have
.begin nofill turnon "∂"
.n←8 ;m←48

∂(n)⊗⊗w=u . w1⊗ 
∂(n)⊗⊗length w1 = m ⊗∂(m)by $LENGTH  
∂(n)⊗⊗listlist w1 ⊗ ∂(m)by {eqn listlist}
∂(n)⊗⊗combine w1 = <qa v>*qd v⊗ ∂(m)since ⊗⊗combine qd w = v⊗
∂(n)⊗⊗<qa v>*qda w1=qa w1 ∧ qda w1*combine qd w1=qd v⊗∂(m)by {eqn combineeqn} and properties of ⊗append 
.end

thus we see that ⊗⊗ispartn[<qa v>,qd v,w1,m-$$1$]⊗
and by induction ⊗⊗w1εpartn[<qa v>,qd v,m-$$1$]⊗.   Thus 
⊗⊗wεtack[u,partn[<qa v>,qd v,m-$$1$]]⊗.   

	In the case that ⊗u1 is not qNIL then  it is easy to see that
⊗⊗ispartn[u*<qa v>,qd v,w,m]⊗.  The only possible trick is to prove the
"∃" clause.  This is done by taking ⊗u1 in the latter case to be qqd of
the ⊗u1 guaranteed to exist by the fact that ⊗⊗ispartn[u,v,w,m]⊗.
Therefore by induction we have ⊗⊗wεpartn[u*<qa v>,qd v,m]⊗ which completes the
proof.  


.cb Exercises
.item←0

#.  Prove the lemmas {eqn partlem0} to {eqn partlem4}.

#.  Prove the remaining criterion {eqn partone} for correctness of ⊗partition.  
.ss(partfunrule,Partial functions and the Minimization Schema.)

	So far we have dealt only with recursive programs that defined 
total functions on S-expressions.   In these cases the functional equation
corresponding to the recursive definition completely characterized the
function on S-expressions.  Frequently we are interested in a program
that does not always terminate and in this case there are likely to 
be many functions that satisfy the corresponding functional equation.
What ever we prove using this equation will be true
for all of these functions, but there are also facts about the
function we intend to define that will not be provable using only
the functional equation.  
For example, the program

!fcnloop&2 ⊗⊗⊗loop x ← loop x			⊗

leads to the sentence

!eqnloopax2 ⊗⊗⊗∀x: [loop x = loop x]		⊗

which provides no information (all functions satisfy it) 
although the function ⊗loop corresponding to the program is undefined for all ⊗x.  
This is not always the case.   Recall the program

!fcnomega&1 ⊗⊗⊗omega x ← [omega x] . qNIL		⊗

which has the functional equation

!eqnomegaax1 ⊗⊗⊗∀x: [omega x = [omega x] . qNIL] .	⊗

We showed (informally) in qsect {subsection appendpf}
that assuming ⊗⊗issexp omega x⊗ leads to
a contradiction thus we can show
⊗⊗∀x: [¬issexp omega x]⊗, using the functional equation and induction.

	In order to characterize recursive programs, we need some
way of expressing the fact that the function we mean is
the least defined solution of the functional equation.   We will do
this by introducing, in addition to the functional equation, a
schema called the ⊗minimization_schema which expresses the fact that
every function satisfying the equation is defined at least every where that
the function assigned to the program is defined, and has the same value
in those cases.

	Recall the general form for a recursive definition

!eqnpdef2  ⊗⊗⊗f x ← qt[f,x] 		⊗

and the corredsponing functional equation

!eqnpdefeq  ⊗⊗⊗∀x: f x = qt[f,x] .	        ⊗

The minimization schema for this form of recursive definition has the form

!eqnminsch ⊗⊗⊗∀x: [issexp qt[F] x ⊃ F x = qt[F] x] ⊃ ∀x: [issexp f x ⊃ f x = F x] ⊗.

Here ⊗F is a function parameter.   This schema is really ⊗schema_schema, 
since for any particular term qt and function symbol ⊗f we produce
from the schema a formula that still contains the paramater ⊗F.  
We then must substitute some function expression of our language for ⊗F 
to produce an axiom.  (This is similar to the induction schemas, except
there we substituted formulas for predicate parameters.)

	The simplest application of the minimization schema is to show that 
the program for ⊗loop given above computes the totally undefined function.
The minimization schema for loop is

!eqnloopminsch ⊗⊗⊗∀x:[issexp F x ⊃ F x = F x] ⊃ ∀x: [issexp loop x ⊃ loop x = F x] ⊗.

If we let ⊗F be the function expression λx: qb then we obtain the 
axiom

⊗⊗⊗∀x:[issexp qb ⊃ qb = qb] ⊃ ∀x: [issexp loop x ⊃ loop x = qb] ⊗.

The left side of the implication is identically true.  
Thus we have

⊗⊗⊗∀x: [issexp loop x ⊃ loop x = qb] ⊗.

If we assume ⊗⊗issexp loop x⊗ we find that issexp qb which contradicts 
$SEXP3.  Thus we have shown 

⊗⊗⊗∀x: ¬issepx loop x                ⊗

as desired.

	The minimization schema provides an alternate method for proving the 
correctness of ⊗samefringe.  To simplify matters we eliminate the auxiliary
function ⊗same from the definition of ⊗samefringe thus eliminating the problem
of having to deal with mutually recursive programs.  The functional defining
⊗samefringe now becomes
.NOFILL

⊗⊗⊗qt%4sf%* = λf: λx y: [[x equal y] or [[not atom x and not atom y] and 			⊗
⊗⊗⊗		[[qa gopher x equal qa gopher y] and f[qd gopher x, qd gopher y]]]] ⊗.
.FILL

Now we form an axiom schema from the minimization schema by using the qt%4sf%*
given above and ⊗samefringe for ⊗f. 
We instantiate this schema with 

⊗⊗⊗F[x, y] = fringe x eq fringe y  .		⊗

.XGENLINES←XGENLINES-2

The proof then consists of the following steps
.begin nofill

	1) 	⊗⊗∀x y: [issexp qt%4sf%*[F] [x, y]]⊗
	2)	⊗⊗∀x y: [F[x, y] = qt%4sf%*[F] [x, y]]⊗
	3)	⊗⊗∀x y:[issexp samefringef[x,y]⊗
.end
from 1) - 3) and the axiom instantiation we conclude

	4)	⊗⊗∀x y: [fringe x equal fringe y = samefringef[x, y]]⊗

from the definition of ⊗samefringe and 4) we conclude

	5)	⊗⊗∀x y: [samefringe[x, y] ≡ fringe x = fringe y]⊗

as desired.


	The minimization schema can sometimes be used to show partial
correctness.  For example, the well known 91-function is defined by
the recursive program over the integers

⊗⊗⊗f%491%* x ← qif x > 100 qthen x - 10 qelse f%491%* f%491%* [x + 11] ⊗.

The goal is to show that

⊗⊗⊗∀x: [f%491%* x = qif x > 100 qthen x - 10 qelse 91] .	⊗

We apply the minimization schema with

⊗⊗⊗F x = qif x > 100 qthen x - 10 qelse 91 ,		⊗

and it can be shown by an explicit calculation without induction that
the premise of the schema is satisfied, and this shows that ⊗⊗f%491%*⊗, 
whenever defined has the desired value.

	The method of ⊗recursion ⊗induction is also
an immediate application of the minimization schema.  If we show
that two functions satisfy the schema of a recursive program, we
show that they both equal the function computed by the program 
wherever the function is defined.

	The utility of the minimization schema for proving partial
correctness or non-termination depends on our ability to name
suitable comparison functions.  ⊗loop and ⊗⊗f%491%*⊗ were easily treated,
because the necessary comparison functions could be given explicitly
without recursion.  Any extension of the language that provides new
tools for naming comparison functions, e.g. going to higher order
logic, will improve our ability to use the schema in proofs.

.next page
.ss(provinex1, Exercises Part 1.)
.item←0

	The following are properties to prove about programs that
you have written.  The functions and predicates referred to are
described in the Exercises of Chapter {subSECTION WRITINex!}.   You 
should carry out the proofs for your definitions of the indicated functions
or predicates.  You may decide to rewrite your definition because (1) you
find that your function definition is not correct or (2) another definition
is cleaner and more amenable to proofs.  This is quite natural if you are
not thinking in terms of proving it correct when you write the definition.


#. Lists
.begin nofill

	##. ⊗⊗∀u. samelength[u,reverse u]⊗

	##. ⊗⊗∀u v:istail[commontail[u,v],v]⊗
	##. ⊗⊗∀u v:istail[commontail[u,v],u]⊗

	##. ⊗⊗∀u v: commontail[u,v]=commontail[v,u]⊗

	##. ⊗⊗∀u v:[append[upto[commontail[u,v],v],commontail[u,v]]=v]⊗
	##. ⊗⊗∀u v:[append[upto[commontail[u,v],u],commontail[u,v]]=u]⊗

Note that ⊗istail has already been worked on in earlier exercises.  
.end


#. Sexpressions

	##. ⊗⊗∀x y:[x = get[y,point[x,y]]]⊗

	##. ⊗⊗∀x:[balanced[balance[x]] samefringe[balance[x],x]]⊗

#. Algebra and arithmetic

	##. ⊗⊗∀u v: poly u ∧ poly v ⊃ sum[prod[quot[u,v],v],rem[u,v]⊗

	##. ⊗⊗∀x: arith x ⊃ numval[sop x]]=numval[x]⊗

	Part of the exercise is to invent suitable predicates ⊗poly and ⊗arith
which characterize the domain on which the functions are valid.

#. Sets

	##. ⊗⊗∀x u v:[xε[u∪v] ⊃ xεu ∨ xεv]⊗

	##. ⊗⊗∀x u v:[[xεu] ⊃ ¬xε[v - u]]⊗


#. Permutations

	##. ⊗⊗∀u:[lcycle rcycle u = u]⊗

	##. ⊗⊗∀u:[isperm1 u ⊃ [compose1[p,invert1[p]] = id1⊗

	##. ⊗⊗∀u:[isperm1 u ⊃ [compose1[invert1[p],p] = id1⊗

	##. ⊗⊗u: [isperm1 u ⊃ [invert1 invert1 p = p]]⊗

	##. ⊗⊗∀u v:[isperm2 u ∧ isperm2 v ⊃ rho21[compose2[u,v]] = compose1[rho21 u,rho21 v2]]⊗

.ss(provinex2,Exercises Part2.)
.item←0

	This collection of exercises treats properties of association
lists, substitutions, and pattern matching.  These topics are strongly
interrelated and the ability to treat properties of
such programs is fundamental to the general area of symbolic computation.



#. Association lists

	Prove the following facts about association lists.
.begin nofill

	##.	⊗⊗∀u v: [alist u ∧ alist v ⊃ alist[u * v]⊗

	##. 	⊗⊗∀z u v: alist u ∧ alist v ⊃ ⊗
                          ⊗⊗[assoc[z,u*v] = qif qn assoc[z,u] qthen assoc[z,v] qelse assoc[z,u]]⊗

where

     	⊗⊗alist u ← qn u ∨ [¬qat qa u ∧ alist qd u]]]⊗ 

	⊗⊗assoc[x, s] ← qif qn s qthen qNIL qelse qif x = qaa s qthen qa s qelse assoc[x, qd s]⊗
.end

#. Properties of substitutions and substitution lists.

	With function definitions as given below,
⊗⊗subst[x,_y,_z]⊗ is the result of replacing the variable ⊗y by the
S-expression ⊗x wherever ⊗y occurs in ⊗z.  If ⊗s is a list of substitutions of 
the form ⊗⊗y_._x⊗ then ⊗⊗sublis[z,_s]⊗ is the result of "simultaneously" performing
all of the substitutions on the list to ⊗z. If ⊗s1 and ⊗s2 are lists of substitutions
then ⊗s1 @ ⊗s2 is the "composition"  of the two.  Prove the following properties.

.NOFILL

	##.	⊗⊗∀x y z: subst[x, y, z] = sublis[z, <y . x>]⊗

	##.	⊗⊗∀z s1 s2: sublis[z, s1 @ s2] = sublis[sublis[z, s1], s2]⊗

	##. 	⊗⊗∀z s1 s2 s3: sublis[z, s1 @ [s2 @ s3]] = sublis[z, [s1 @ s2] @ s3]⊗

.<<	##.	⊗⊗∀x y z: (¬occur[y, z] ⊃ subst[x, y, z] = z)⊗ 
.>>
	##.	⊗⊗∀x x1 y y1 z: ((y ≠  y1 ∧ ¬occur[y, x1]) ⊃ ⊗
	    		⊗⊗subst[x1, y1, subst[x, y, z]] = subst[subst[x1, y1, x], y, subst[x1, y1, z]])⊗


where

	⊗⊗subst[x, y, z] ← qif qat z qthen [qif y = z qthen x qelse z] ⊗
			⊗⊗qelse subst[x, y, qa z] . subst[x, y, qd z]⊗

.<<	⊗⊗occur[x, y] ← [x = y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x, qd y]]]⊗. 
.>>
	⊗⊗sublis[x, s] ← qif qat x qthen α{assoc[x, s]α}[λz: qif qn z qthen x qelse qd z]⊗
			⊗⊗qelse sublis[qa x, s] . sublis[qd x, s]⊗

	⊗⊗s1 @ s2 ← subsub[s1, s2] * s2⊗

	⊗⊗subsub[s1, s2] ← qif qn s1 qthen qNIL qelse [qaa s1 . sublis[qda s1, s2]] . subsub[qd s1, s2]⊗
.FILL

#.  Pattern matching 


	The function ⊗inst is one sort of "pattern matcher".  We say that an
S-expression ⊗x is an instance of another S-expression ⊗y if ⊗y can be transformed
into ⊗x by replacing some of the atoms of ⊗y which satisfy ⊗isvar by suitable
values.  (All occurrences of the same variable should be replaced by the
same value.)  ⊗⊗inst[x,_y,_qNIL]⊗ is
$NO if ⊗x is not and instance of the pattern ⊗y, and otherwise is the list of
substitions which will convert ⊗y into ⊗x.  In the latter case we have
⊗⊗x_=_sublis[y,_inst[x,_y,_qNIL]⊗.  Write a definition for ⊗inst and prove that

⊗⊗⊗∀x y u: (inst[x, y, u] ≠ $NO ⊃ x = sublis[y, inst[x, y, u]])⊗

.if false then begin "inst"

	⊗⊗inst[x, y, s] ← qif s = $NO qthen $NO ⊗
		⊗⊗qelse qif qat y qthen [qif isvar y qthen ⊗
				⊗⊗α{assoc[y, s]α}[λz: qif qn z qthen [y . x] . s qelse qif qd z = x qthen s qelse $NO ]⊗
			⊗⊗qelse qif y = x qthen s qelse $NO ]⊗
	    	⊗⊗qelse qif qat x qthen $NO ⊗
		⊗⊗qelse inst[qd x, qd y, inst[qa x, qa y, s]]⊗
.end "inst"

#. Unification

	(This is a fairly substantial exercise.)  

	⊗unify[x,y] attempts to find the most general 
pattern which is an instance of both ⊗x and ⊗y. If no such pattern exists the it
returns $NO, otherwise it returns a list of substitutions which will convert both
⊗x and ⊗y into that pattern.  Write a definition of ⊗unify and prove

	##.	⊗⊗∀x y: (unify[x, y] ≠ $NO ⊃ sublis[x, unify[x, y]] = sublis[y, unify[x, y]])⊗

        ##. 	⊗⊗∀x y: (unify[x, y] = $NO ⊃ ∀s: sublis[x, s] ≠ sublis[y, s])⊗

	##.	⊗⊗∀x y s: (sublis[x, s] = sublis[y, s] ⊃ ∃s1: ∀z: sublis[z, s] = sublis[z, unify[x, y] @ s1])⊗



. if false then begin "unify"

 	⊗⊗isvar x ← x = $U ∨ x = $V ∨ x = $W ∨ x = $X ∨ x = $Y ∨ x = $Z ⊗

	⊗⊗unify[x, y] ← qif x = y qthen qNIL⊗
		⊗⊗qelse qif isvar x qthen [qif occur[x, y] qthen $NO qelse <x . y>]⊗
		⊗⊗qelse qif isvar y qthen [qif occur[y, x] qthen $NO qelse <y . x>]⊗
		⊗⊗qelse qif [qat x ∨ qat y] qthen $NO ⊗
		⊗⊗qelse α{unify[qa x,qa y]α}⊗
			⊗⊗[λs1: qif s1 = $NO qthen $NO ⊗
			    ⊗⊗qelse α{unify[sublis[qd x, s1],sublis[qd y, s1]]α}⊗
				⊗⊗[λs2: qif s2 = $NO qthen $NO qelse s1 @ s2]]⊗

.end "unify"